Skip to content

Commit 05ae79c

Browse files
leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
committed
Update lean-toolchain for leanprover/lean4#11220 
2 parents c062e48 + 3dc572b commit 05ae79c

File tree

7,238 files changed

+67357
-32731
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

7,238 files changed

+67357
-32731
lines changed

‎.github/build.in.yml‎

Lines changed: 54 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ jobs:
3838
lint-outcome: ${{ steps.lint.outcome }}
3939
mk_all-outcome: ${{ steps.mk_all.outcome }}
4040
noisy-outcome: ${{ steps.noisy.outcome }}
41-
shake-outcome: ${{ steps.shake.outcome }}
41+
# shake-outcome: ${{ steps.shake.outcome }}
4242
test-outcome: ${{ steps.test.outcome }}
4343
defaults: # On Hoskinson runners, landrun is already installed.
4444
run: # note that .pr-branch/.lake must be created in a step below before we use this
@@ -238,6 +238,51 @@ jobs:
238238
echo "✅ All inputRevs in lake-manifest.json are valid"
239239
fi
240240
241+
- name: verify ProofWidgets lean-toolchain matches on versioned releases
242+
# Only enforce this on the main mathlib4 repository, not on nightly-testing
243+
if: github.repository == 'leanprover-community/mathlib4'
244+
shell: bash
245+
run: |
246+
cd pr-branch
247+
248+
# Read the lean-toolchain file
249+
TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
250+
echo "Lean toolchain: $TOOLCHAIN"
251+
252+
# Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
253+
if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
254+
echo "✓ Detected versioned Lean release: $TOOLCHAIN"
255+
echo "Verifying ProofWidgets lean-toolchain matches..."
256+
257+
# Check if ProofWidgets lean-toolchain exists
258+
if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
259+
echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
260+
echo "This file should be created by 'lake env' during dependency download."
261+
exit 1
262+
fi
263+
264+
# Read ProofWidgets lean-toolchain
265+
PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
266+
echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
267+
268+
# Compare the two
269+
if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
270+
echo "❌ Error: Lean toolchain mismatch!"
271+
echo " Main lean-toolchain: $TOOLCHAIN"
272+
echo " ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
273+
echo ""
274+
echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
275+
echo "the ProofWidgets dependency must use the same toolchain."
276+
echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
277+
exit 1
278+
else
279+
echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
280+
fi
281+
else
282+
echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
283+
echo "Skipping ProofWidgets toolchain verification."
284+
fi
285+
241286
- name: get cache (1/3 - setup and initial fetch)
242287
id: get_cache_part1_setup
243288
shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -412,7 +457,7 @@ jobs:
412457
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
413458

414459
- name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
415-
if: always()
460+
if: ${{ always() && steps.mk_all.outcome != 'skipped' }}
416461
run: |
417462
if [[ "${{ steps.mk_all.outcome }}" != "success" ]]; then
418463
echo "Please run 'lake exe mk_all' to regenerate the import all files"
@@ -443,11 +488,13 @@ jobs:
443488
action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
444489
linters: gcc
445490

446-
- name: check for unused imports
447-
id: shake
448-
run: |
449-
cd pr-branch
450-
env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
491+
# With the arrival of the module system, the old `shake` is no longer functional.
492+
# This will be replaced soon.
493+
# - name: check for unused imports
494+
# id: shake
495+
# run: |
496+
# cd pr-branch
497+
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
451498

452499
- name: lint mathlib
453500
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}

‎.github/workflows/bors.yml‎

Lines changed: 54 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ jobs:
4848
lint-outcome: ${{ steps.lint.outcome }}
4949
mk_all-outcome: ${{ steps.mk_all.outcome }}
5050
noisy-outcome: ${{ steps.noisy.outcome }}
51-
shake-outcome: ${{ steps.shake.outcome }}
51+
# shake-outcome: ${{ steps.shake.outcome }}
5252
test-outcome: ${{ steps.test.outcome }}
5353
defaults: # On Hoskinson runners, landrun is already installed.
5454
run: # note that .pr-branch/.lake must be created in a step below before we use this
@@ -248,6 +248,51 @@ jobs:
248248
echo "✅ All inputRevs in lake-manifest.json are valid"
249249
fi
250250
251+
- name: verify ProofWidgets lean-toolchain matches on versioned releases
252+
# Only enforce this on the main mathlib4 repository, not on nightly-testing
253+
if: github.repository == 'leanprover-community/mathlib4'
254+
shell: bash
255+
run: |
256+
cd pr-branch
257+
258+
# Read the lean-toolchain file
259+
TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
260+
echo "Lean toolchain: $TOOLCHAIN"
261+
262+
# Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
263+
if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
264+
echo "✓ Detected versioned Lean release: $TOOLCHAIN"
265+
echo "Verifying ProofWidgets lean-toolchain matches..."
266+
267+
# Check if ProofWidgets lean-toolchain exists
268+
if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
269+
echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
270+
echo "This file should be created by 'lake env' during dependency download."
271+
exit 1
272+
fi
273+
274+
# Read ProofWidgets lean-toolchain
275+
PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
276+
echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
277+
278+
# Compare the two
279+
if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
280+
echo "❌ Error: Lean toolchain mismatch!"
281+
echo " Main lean-toolchain: $TOOLCHAIN"
282+
echo " ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
283+
echo ""
284+
echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
285+
echo "the ProofWidgets dependency must use the same toolchain."
286+
echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
287+
exit 1
288+
else
289+
echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
290+
fi
291+
else
292+
echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
293+
echo "Skipping ProofWidgets toolchain verification."
294+
fi
295+
251296
- name: get cache (1/3 - setup and initial fetch)
252297
id: get_cache_part1_setup
253298
shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -422,7 +467,7 @@ jobs:
422467
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
423468

424469
- name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
425-
if: always()
470+
if: ${{ always() && steps.mk_all.outcome != 'skipped' }}
426471
run: |
427472
if [[ "${{ steps.mk_all.outcome }}" != "success" ]]; then
428473
echo "Please run 'lake exe mk_all' to regenerate the import all files"
@@ -453,11 +498,13 @@ jobs:
453498
action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
454499
linters: gcc
455500

456-
- name: check for unused imports
457-
id: shake
458-
run: |
459-
cd pr-branch
460-
env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
501+
# With the arrival of the module system, the old `shake` is no longer functional.
502+
# This will be replaced soon.
503+
# - name: check for unused imports
504+
# id: shake
505+
# run: |
506+
# cd pr-branch
507+
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
461508

462509
- name: lint mathlib
463510
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}

‎.github/workflows/build.yml‎

Lines changed: 54 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ jobs:
5555
lint-outcome: ${{ steps.lint.outcome }}
5656
mk_all-outcome: ${{ steps.mk_all.outcome }}
5757
noisy-outcome: ${{ steps.noisy.outcome }}
58-
shake-outcome: ${{ steps.shake.outcome }}
58+
# shake-outcome: ${{ steps.shake.outcome }}
5959
test-outcome: ${{ steps.test.outcome }}
6060
defaults: # On Hoskinson runners, landrun is already installed.
6161
run: # note that .pr-branch/.lake must be created in a step below before we use this
@@ -255,6 +255,51 @@ jobs:
255255
echo "✅ All inputRevs in lake-manifest.json are valid"
256256
fi
257257
258+
- name: verify ProofWidgets lean-toolchain matches on versioned releases
259+
# Only enforce this on the main mathlib4 repository, not on nightly-testing
260+
if: github.repository == 'leanprover-community/mathlib4'
261+
shell: bash
262+
run: |
263+
cd pr-branch
264+
265+
# Read the lean-toolchain file
266+
TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
267+
echo "Lean toolchain: $TOOLCHAIN"
268+
269+
# Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
270+
if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
271+
echo "✓ Detected versioned Lean release: $TOOLCHAIN"
272+
echo "Verifying ProofWidgets lean-toolchain matches..."
273+
274+
# Check if ProofWidgets lean-toolchain exists
275+
if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
276+
echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
277+
echo "This file should be created by 'lake env' during dependency download."
278+
exit 1
279+
fi
280+
281+
# Read ProofWidgets lean-toolchain
282+
PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
283+
echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
284+
285+
# Compare the two
286+
if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
287+
echo "❌ Error: Lean toolchain mismatch!"
288+
echo " Main lean-toolchain: $TOOLCHAIN"
289+
echo " ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
290+
echo ""
291+
echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
292+
echo "the ProofWidgets dependency must use the same toolchain."
293+
echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
294+
exit 1
295+
else
296+
echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
297+
fi
298+
else
299+
echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
300+
echo "Skipping ProofWidgets toolchain verification."
301+
fi
302+
258303
- name: get cache (1/3 - setup and initial fetch)
259304
id: get_cache_part1_setup
260305
shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -429,7 +474,7 @@ jobs:
429474
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
430475

431476
- name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
432-
if: always()
477+
if: ${{ always() && steps.mk_all.outcome != 'skipped' }}
433478
run: |
434479
if [[ "${{ steps.mk_all.outcome }}" != "success" ]]; then
435480
echo "Please run 'lake exe mk_all' to regenerate the import all files"
@@ -460,11 +505,13 @@ jobs:
460505
action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
461506
linters: gcc
462507

463-
- name: check for unused imports
464-
id: shake
465-
run: |
466-
cd pr-branch
467-
env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
508+
# With the arrival of the module system, the old `shake` is no longer functional.
509+
# This will be replaced soon.
510+
# - name: check for unused imports
511+
# id: shake
512+
# run: |
513+
# cd pr-branch
514+
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
468515

469516
- name: lint mathlib
470517
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}

‎.github/workflows/build_fork.yml‎

Lines changed: 54 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ jobs:
5252
lint-outcome: ${{ steps.lint.outcome }}
5353
mk_all-outcome: ${{ steps.mk_all.outcome }}
5454
noisy-outcome: ${{ steps.noisy.outcome }}
55-
shake-outcome: ${{ steps.shake.outcome }}
55+
# shake-outcome: ${{ steps.shake.outcome }}
5656
test-outcome: ${{ steps.test.outcome }}
5757
defaults: # On Hoskinson runners, landrun is already installed.
5858
run: # note that .pr-branch/.lake must be created in a step below before we use this
@@ -252,6 +252,51 @@ jobs:
252252
echo "✅ All inputRevs in lake-manifest.json are valid"
253253
fi
254254
255+
- name: verify ProofWidgets lean-toolchain matches on versioned releases
256+
# Only enforce this on the main mathlib4 repository, not on nightly-testing
257+
if: github.repository == 'leanprover-community/mathlib4'
258+
shell: bash
259+
run: |
260+
cd pr-branch
261+
262+
# Read the lean-toolchain file
263+
TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
264+
echo "Lean toolchain: $TOOLCHAIN"
265+
266+
# Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
267+
if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
268+
echo "✓ Detected versioned Lean release: $TOOLCHAIN"
269+
echo "Verifying ProofWidgets lean-toolchain matches..."
270+
271+
# Check if ProofWidgets lean-toolchain exists
272+
if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
273+
echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
274+
echo "This file should be created by 'lake env' during dependency download."
275+
exit 1
276+
fi
277+
278+
# Read ProofWidgets lean-toolchain
279+
PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
280+
echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
281+
282+
# Compare the two
283+
if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
284+
echo "❌ Error: Lean toolchain mismatch!"
285+
echo " Main lean-toolchain: $TOOLCHAIN"
286+
echo " ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
287+
echo ""
288+
echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
289+
echo "the ProofWidgets dependency must use the same toolchain."
290+
echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
291+
exit 1
292+
else
293+
echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
294+
fi
295+
else
296+
echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
297+
echo "Skipping ProofWidgets toolchain verification."
298+
fi
299+
255300
- name: get cache (1/3 - setup and initial fetch)
256301
id: get_cache_part1_setup
257302
shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -426,7 +471,7 @@ jobs:
426471
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
427472

428473
- name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
429-
if: always()
474+
if: ${{ always() && steps.mk_all.outcome != 'skipped' }}
430475
run: |
431476
if [[ "${{ steps.mk_all.outcome }}" != "success" ]]; then
432477
echo "Please run 'lake exe mk_all' to regenerate the import all files"
@@ -457,11 +502,13 @@ jobs:
457502
action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
458503
linters: gcc
459504

460-
- name: check for unused imports
461-
id: shake
462-
run: |
463-
cd pr-branch
464-
env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
505+
# With the arrival of the module system, the old `shake` is no longer functional.
506+
# This will be replaced soon.
507+
# - name: check for unused imports
508+
# id: shake
509+
# run: |
510+
# cd pr-branch
511+
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
465512

466513
- name: lint mathlib
467514
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}

0 commit comments

Comments
 (0)