Skip to content

Commit 2ca4d81

Browse files
VierkantorVierkantor
committed
feat(CI): use lean-action's "reinstall transient toolchain" step (#24305)
We had a hand-coded "reinstall transient toolchain" step in a few workflows. I added this to `lean-action` so we can call it directly from that action. We can also skip the "print lean and lake versions" step since `lean-action` does that too. This PR also upgrades the `lean-action` version to the latest `main` branch.
1 parent 5eed989 commit 2ca4d81

14 files changed

+25
-96
lines changed

‎.github/build.in.yml

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ jobs:
5757
python-version: 3.8
5858

5959
- name: Configure Lean
60-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
60+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
6161
with:
6262
auto-config: false
6363
use-github-cache: false
@@ -101,23 +101,12 @@ jobs:
101101
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
102102

103103
- name: Configure Lean
104-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
104+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
105105
with:
106106
auto-config: false
107107
use-github-cache: false
108108
use-mathlib-cache: false
109-
110-
- name: If using a lean-pr-release toolchain, uninstall
111-
run: |
112-
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
113-
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
114-
elan toolchain uninstall "$(cat lean-toolchain)"
115-
fi
116-
117-
- name: print lean and lake versions
118-
run: |
119-
lean --version
120-
lake --version
109+
reinstall-transient-toolchain: true
121110

122111
- name: cleanup .cache/mathlib
123112
run: |

‎.github/workflows/add_label_from_diff.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ jobs:
2525
with:
2626
fetch-depth: 0
2727
- name: Configure Lean
28-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
28+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
2929
with:
3030
auto-config: false
3131
use-github-cache: false

‎.github/workflows/bench_summary_comment.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ jobs:
1717
scripts/bench_summary.lean
1818
1919
- name: Configure Lean
20-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
20+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
2121
with:
2222
auto-config: false
2323
use-github-cache: false

‎.github/workflows/bors.yml

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ jobs:
6767
python-version: 3.8
6868

6969
- name: Configure Lean
70-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
70+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
7171
with:
7272
auto-config: false
7373
use-github-cache: false
@@ -111,23 +111,12 @@ jobs:
111111
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
112112

113113
- name: Configure Lean
114-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
114+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
115115
with:
116116
auto-config: false
117117
use-github-cache: false
118118
use-mathlib-cache: false
119-
120-
- name: If using a lean-pr-release toolchain, uninstall
121-
run: |
122-
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
123-
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
124-
elan toolchain uninstall "$(cat lean-toolchain)"
125-
fi
126-
127-
- name: print lean and lake versions
128-
run: |
129-
lean --version
130-
lake --version
119+
reinstall-transient-toolchain: true
131120

132121
- name: cleanup .cache/mathlib
133122
run: |

‎.github/workflows/bot_fix_style.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ jobs:
117117
python-version: 3.8
118118

119119
- name: Configure Lean
120-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
120+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
121121
with:
122122
auto-config: false
123123
use-github-cache: false

‎.github/workflows/build.yml

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ jobs:
7474
python-version: 3.8
7575

7676
- name: Configure Lean
77-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
77+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
7878
with:
7979
auto-config: false
8080
use-github-cache: false
@@ -118,23 +118,12 @@ jobs:
118118
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
119119

120120
- name: Configure Lean
121-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
121+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
122122
with:
123123
auto-config: false
124124
use-github-cache: false
125125
use-mathlib-cache: false
126-
127-
- name: If using a lean-pr-release toolchain, uninstall
128-
run: |
129-
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
130-
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
131-
elan toolchain uninstall "$(cat lean-toolchain)"
132-
fi
133-
134-
- name: print lean and lake versions
135-
run: |
136-
lean --version
137-
lake --version
126+
reinstall-transient-toolchain: true
138127

139128
- name: cleanup .cache/mathlib
140129
run: |

‎.github/workflows/build_fork.yml

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ jobs:
7171
python-version: 3.8
7272

7373
- name: Configure Lean
74-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
74+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
7575
with:
7676
auto-config: false
7777
use-github-cache: false
@@ -115,23 +115,12 @@ jobs:
115115
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
116116

117117
- name: Configure Lean
118-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
118+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
119119
with:
120120
auto-config: false
121121
use-github-cache: false
122122
use-mathlib-cache: false
123-
124-
- name: If using a lean-pr-release toolchain, uninstall
125-
run: |
126-
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
127-
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
128-
elan toolchain uninstall "$(cat lean-toolchain)"
129-
fi
130-
131-
- name: print lean and lake versions
132-
run: |
133-
lean --version
134-
lake --version
123+
reinstall-transient-toolchain: true
135124

136125
- name: cleanup .cache/mathlib
137126
run: |

‎.github/workflows/daily.yml

Lines changed: 2 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -56,23 +56,12 @@ jobs:
5656
ref: ${{ env.BRANCH_REF }}
5757

5858
- name: Configure Lean
59-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
59+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
6060
with:
6161
auto-config: false
6262
use-github-cache: false
6363
use-mathlib-cache: false
64-
65-
- name: If using a lean-pr-release toolchain, uninstall
66-
run: |
67-
if [[ "$(cat lean-toolchain)" =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
68-
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
69-
elan toolchain uninstall "$(cat lean-toolchain)"
70-
fi
71-
72-
- name: Print Lean and Lake versions
73-
run: |
74-
lean --version
75-
lake --version
64+
reinstall-transient-toolchain: true
7665

7766
- name: Run lake exe cache get
7867
run: |

‎.github/workflows/discover-lean-pr-testing.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ jobs:
2525
git config --global user.email "github-actions@github.com"
2626
2727
- name: Configure Lean
28-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
28+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
2929
with:
3030
auto-config: false
3131
use-github-cache: false

‎.github/workflows/latest_import.yml

Lines changed: 2 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -28,23 +28,12 @@ jobs:
2828
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
2929

3030
- name: Configure Lean
31-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
31+
uses: leanprover/lean-action@e18f2df7f0d4f30d11a4b963bff9b1140999480c # 2025-04-22
3232
with:
3333
auto-config: false
3434
use-github-cache: false
3535
use-mathlib-cache: false
36-
37-
- name: If using a lean-pr-release toolchain, uninstall
38-
run: |
39-
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
40-
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
41-
elan toolchain uninstall "$(cat lean-toolchain)"
42-
fi
43-
44-
- name: print lean and lake versions
45-
run: |
46-
lean --version
47-
lake --version
36+
reinstall-transient-toolchain: true
4837

4938
- name: add minImports linter option
5039
run: |

0 commit comments

Comments
 (0)