Skip to content

Commit fff5a28

Browse files
kim-emkim-em
committed
chore: CI detects ProofWidgets toolchain mismatch (leanprover-community#31723)
See zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/ProofWidgets.20not.20building.2C.20says.20it.20is.20out.20of.20date/near/556720459 Ideally, this would fail right now, demonstrating that it is working, but of course CI only runs from the `master` version. Update: now that leanprover-community#31720 is in, this can be merged.
1 parent 61abd2f commit fff5a28

File tree

4 files changed

+180
-0
lines changed

4 files changed

+180
-0
lines changed

‎.github/build.in.yml‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -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

‎.github/workflows/bors.yml‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -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

‎.github/workflows/build.yml‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -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

‎.github/workflows/build_fork.yml‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -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

0 commit comments

Comments
 (0)
⚡