@@ -222,7 +222,7 @@ jobs:
222222
223223name : validate lake-manifest.json inputRevs
224224 # Only enforce this on the main mathlib4 repository, not on nightly-testing
225- if : github.repository == 'leanprover-community/mathlib4'
225+ if : github.repository == 'leanprover-community/mathlib4' && github.ref_name != 'nightly-testing'
226226 shell : bash
227227 run : |
228228 cd pr-branch
@@ -247,76 +247,6 @@ jobs:
247247 echo "✅ All inputRevs in lake-manifest.json are valid"
248248 fi
249249
250- name : validate ProofWidgets source repository
251- # Only enforce this on the main mathlib4 repository, not on nightly-testing
252- if : github.repository == 'leanprover-community/mathlib4'
253- shell : bash
254- run : |
255- cd pr-branch
256-
257- expected_url='https://github.com/leanprover-community/ProofWidgets4'
258- proofwidgets_count=$(jq '[.packages[] | select(.name == "proofwidgets")] | length' lake-manifest.json)
259- if [ "$proofwidgets_count" -ne 1 ]; then
260- echo "❌ Error: expected exactly one proofwidgets entry in lake-manifest.json, found $proofwidgets_count"
261- exit 1
262- fi
263-
264- proofwidgets_url=$(jq -r '.packages[] | select(.name == "proofwidgets") | .url' lake-manifest.json)
265- normalized_url="${proofwidgets_url%.git}"
266- if [ "$normalized_url" != "$expected_url" ]; then
267- echo "❌ Error: invalid ProofWidgets source URL in lake-manifest.json"
268- echo " expected: $expected_url"
269- echo " found: $proofwidgets_url"
270- exit 1
271- fi
272-
273- echo "✅ ProofWidgets source URL is allowed: $proofwidgets_url"
274-
275- name : verify ProofWidgets lean-toolchain matches on versioned releases
276- # Only enforce this on the main mathlib4 repository, not on nightly-testing
277- if : github.repository == 'leanprover-community/mathlib4'
278- shell : bash
279- run : |
280- cd pr-branch
281-
282- # Read the lean-toolchain file
283- TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
284- echo "Lean toolchain: $TOOLCHAIN"
285-
286- # Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
287- if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
288- echo "✓ Detected versioned Lean release: $TOOLCHAIN"
289- echo "Verifying ProofWidgets lean-toolchain matches..."
290-
291- # Check if ProofWidgets lean-toolchain exists
292- if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
293- echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
294- echo "This file should be created by 'lake env' during dependency download."
295- exit 1
296- fi
297-
298- # Read ProofWidgets lean-toolchain
299- PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
300- echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
301-
302- # Compare the two
303- if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
304- echo "❌ Error: Lean toolchain mismatch!"
305- echo " Main lean-toolchain: $TOOLCHAIN"
306- echo " ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
307- echo ""
308- echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
309- echo "the ProofWidgets dependency must use the same toolchain."
310- echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
311- exit 1
312- else
313- echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
314- fi
315- else
316- echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
317- echo "Skipping ProofWidgets toolchain verification."
318- fi
319-
320250name : get cache (1/3 - setup and initial fetch)
321251 id : get_cache_part1_setup
322252 shell : bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
@@ -327,7 +257,7 @@ jobs:
327257
328258 # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
329259 echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
330- ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Mathlib/Init.lean
260+ ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
331261
332262name : get cache (2/3 - test Mathlib.Init cache)
333263 id : get_cache_part2_test
@@ -380,13 +310,19 @@ jobs:
380310 # cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
381311 echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
382312 if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
383- git checkout "$PREV_SHA"
384- ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
385- # Run again with --repo, to ensure we actually get the oleans.
386- ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
387-
388- echo "Switching back to branch head"
389- git checkout "$ORIG_SHA"
313+ # Skip warmup if the previous commit uses a different toolchain
314+ PREV_TOOLCHAIN=$(git show "$PREV_SHA:lean-toolchain" 2>/dev/null || true)
315+ if [[ "$PREV_TOOLCHAIN" != "$(cat lean-toolchain)" ]]; then
316+ echo "Previous commit $PREV_SHA uses a different toolchain ($PREV_TOOLCHAIN); skipping warmup."
317+ else
318+ git checkout "$PREV_SHA"
319+ ../tools-branch/.lake/build/bin/cache get
320+ # Run again with --repo, to ensure we actually get the oleans.
321+ ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
322+
323+ echo "Switching back to branch head"
324+ git checkout "$ORIG_SHA"
325+ fi
390326 else
391327 echo "Could not fetch $PREV_SHA; skipping parent warmup cache fetch."
392328 fi
@@ -396,18 +332,10 @@ jobs:
396332
397333 echo "Fetching all remaining cache..."
398334
399- ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
335+ ../tools-branch/.lake/build/bin/cache get
400336
401337 # Run again with --repo, to ensure we actually get the oleans.
402- ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
403-
404- name : fetch ProofWidgets release
405- # We need network access for ProofWidgets frontend assets.
406- # Run inside landrun so PR-controlled code remains sandboxed.
407- shell : landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
408- run : |
409- cd pr-branch
410- lake build proofwidgets:release
338+ ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
411339
412340name : update {Mathlib, Tactic, Counterexamples, Archive}.lean
413341 id : mk_all
@@ -462,8 +390,8 @@ jobs:
462390 shell : bash
463391 run : |
464392 cd pr-branch
465- ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Archive.lean
466- ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Counterexamples.lean
393+ ../tools-branch/.lake/build/bin/cache get Archive.lean
394+ ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
467395
468396name : build archive
469397 id : archive
@@ -523,7 +451,7 @@ jobs:
523451
524452name : upload cache staging artifact
525453 if : ${{ always() && steps.cache_staging_check.outputs.has_files == 'true' }}
526- uses : actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
454+ uses : actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
527455 with :
528456 name : cache-staging
529457 path : cache-staging/
@@ -646,12 +574,14 @@ jobs:
646574 - name : Generate lean-pr-testing app token
647575 if : ${{ always() && github.repository == 'leanprover-community/mathlib4-nightly-testing' && (startsWith(github.ref_name, 'lean-pr-testing-') || startsWith(github.ref_name, 'batteries-pr-testing-')) }}
648576 id : lean-pr-testing-token
649- uses : actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2 .1
577+ uses : actions/create-github-app-token@1b10c78c7865c340bc4f6099eb2f838309f1e8c3 # v3.1 .1
650578 with :
651- app-id : ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
652- private-key : ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
653- owner : leanprover
654- repositories : lean4
579+ # `batteries-pr-testing-*` branches need a token scoped to `leanprover-community/batteries`
580+ # for the labelling API; `lean-pr-testing-*` branches need one scoped to `leanprover/lean4`.
581+ app-id : ${{ startsWith(github.ref_name, 'batteries-pr-testing-') && secrets.MATHLIB_NIGHTLY_TESTING_APP_ID || secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
582+ private-key : ${{ startsWith(github.ref_name, 'batteries-pr-testing-') && secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY || secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
583+ owner : ${{ startsWith(github.ref_name, 'batteries-pr-testing-') && 'leanprover-community' || 'leanprover' }}
584+ repositories : ${{ startsWith(github.ref_name, 'batteries-pr-testing-') && 'batteries' || 'lean4' }}
655585 # The create-github-app-token README states that this token is masked and will not be logged accidentally.
656586 - name : Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
657587 if : ${{ always() && github.repository == 'leanprover-community/mathlib4-nightly-testing' && (startsWith(github.ref_name, 'lean-pr-testing-') || startsWith(github.ref_name, 'batteries-pr-testing-')) }}
@@ -690,7 +620,7 @@ jobs:
690620 fetch-depth : 1
691621
692622 - name : Configure Lean
693- uses : leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4 .0
623+ uses : leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5 .0
694624 with :
695625 auto-config : false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
696626 use-github-cache : false
@@ -708,7 +638,7 @@ jobs:
708638 echo "CACHE_BIN=$CACHE_BIN" >> "$GITHUB_ENV"
709639
710640name : Download cache staging artifact
711- uses : actions/download-artifact@70fc10c6e5e1ce46ad2ea6f2b72d43f7d47b13c3 # v8.0.0
641+ uses : actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
712642 with :
713643 name : cache-staging
714644 path : cache-staging
@@ -761,7 +691,7 @@ jobs:
761691 ref : ${{ inputs.pr_branch_ref }}
762692
763693 - name : Configure Lean
764- uses : leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4 .0
694+ uses : leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5 .0
765695 with :
766696 auto-config : false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
767697 use-github-cache : false
@@ -804,7 +734,7 @@ jobs:
804734 lake exe graph
805735
806736name : upload the import graph
807- uses : actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
737+ uses : actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
808738 with :
809739 name : import-graph
810740 path : import_graph.dot
@@ -815,6 +745,12 @@ jobs:
815745 - name : clean up the import graph file
816746 run : rm import_graph.dot
817747
748+ - name : check all scripts build successfully
749+ run : |
750+ lake env lean scripts/create_deprecated_modules.lean
751+ lake env lean scripts/autolabel.lean
752+ lake exe check_title_labels --labels "t-algebra" "feat: dummy PR for testing"
753+
818754name : build everything
819755 # make sure everything is available for test/import_all.lean
820756 # and that miscellaneous executables still work
@@ -937,9 +873,10 @@ jobs:
937873if : >- # bot usernames will cause this step to error with "Could not resolve to a User..."
938874 contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
939875 steps.get-label-actor.outputs.username != 'mathlib-nolints' &&
940- steps.get-label-actor.outputs.username != 'mathlib-update-dependencies'
876+ steps.get-label-actor.outputs.username != 'mathlib-update-dependencies' &&
877+ steps.get-label-actor.outputs.username != 'mathlib-splicebot'
941878 name: check team membership
942- uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3 .0.0
879+ uses: tspascoal/get-user-teams-membership@818140d631d5f29f26b151afbe4179f87d9ceb5e # v4 .0.1
943880 id: actorTeams
944881 with:
945882 organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
@@ -952,7 +889,9 @@ jobs:
952889 (
953890 steps.get-label-actor.outputs.username == 'mathlib-nolints' ||
954891 steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' ||
892+ steps.get-label-actor.outputs.username == 'mathlib-splicebot' ||
955893 contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') ||
894+ contains(steps.actorTeams.outputs.teams, 'lean-release-managers') ||
956895 contains(steps.actorTeams.outputs.teams, 'bot-users')
957896 )
958897 name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
0 commit comments