@@ -310,13 +310,19 @@ jobs:
310310 # cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
311311 echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
312312 if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
313- git checkout "$PREV_SHA"
314- ../tools-branch/.lake/build/bin/cache get
315- # Run again with --repo, to ensure we actually get the oleans.
316- ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
317-
318- echo "Switching back to branch head"
319- 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
320326 else
321327 echo "Could not fetch $PREV_SHA; skipping parent warmup cache fetch."
322328 fi
@@ -445,7 +451,7 @@ jobs:
445451
446452name : upload cache staging artifact
447453 if : ${{ always() && steps.cache_staging_check.outputs.has_files == 'true' }}
448- uses : actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
454+ uses : actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
449455 with :
450456 name : cache-staging
451457 path : cache-staging/
@@ -568,12 +574,14 @@ jobs:
568574 - name : Generate lean-pr-testing app token
569575 if : ${{ always() && github.repository == 'leanprover-community/mathlib4-nightly-testing' && (startsWith(github.ref_name, 'lean-pr-testing-') || startsWith(github.ref_name, 'batteries-pr-testing-')) }}
570576 id : lean-pr-testing-token
571- uses : actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2 .1
577+ uses : actions/create-github-app-token@1b10c78c7865c340bc4f6099eb2f838309f1e8c3 # v3.1 .1
572578 with :
573- app-id : ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
574- private-key : ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
575- owner : leanprover
576- 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' }}
577585 # The create-github-app-token README states that this token is masked and will not be logged accidentally.
578586 - name : Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
579587 if : ${{ always() && github.repository == 'leanprover-community/mathlib4-nightly-testing' && (startsWith(github.ref_name, 'lean-pr-testing-') || startsWith(github.ref_name, 'batteries-pr-testing-')) }}
@@ -612,7 +620,7 @@ jobs:
612620 fetch-depth : 1
613621
614622 - name : Configure Lean
615- uses : leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4 .0
623+ uses : leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5 .0
616624 with :
617625 auto-config : false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
618626 use-github-cache : false
@@ -630,7 +638,7 @@ jobs:
630638 echo "CACHE_BIN=$CACHE_BIN" >> "$GITHUB_ENV"
631639
632640name : Download cache staging artifact
633- uses : actions/download-artifact@70fc10c6e5e1ce46ad2ea6f2b72d43f7d47b13c3 # v8.0.0
641+ uses : actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
634642 with :
635643 name : cache-staging
636644 path : cache-staging
@@ -683,7 +691,7 @@ jobs:
683691 ref : ${{ inputs.pr_branch_ref }}
684692
685693 - name : Configure Lean
686- uses : leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4 .0
694+ uses : leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5 .0
687695 with :
688696 auto-config : false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
689697 use-github-cache : false
@@ -726,7 +734,7 @@ jobs:
726734 lake exe graph
727735
728736name : upload the import graph
729- uses : actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
737+ uses : actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
730738 with :
731739 name : import-graph
732740 path : import_graph.dot
@@ -737,6 +745,12 @@ jobs:
737745 - name : clean up the import graph file
738746 run : rm import_graph.dot
739747
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+
740754name : build everything
741755 # make sure everything is available for test/import_all.lean
742756 # and that miscellaneous executables still work
@@ -862,7 +876,7 @@ jobs:
862876 steps.get-label-actor.outputs.username != 'mathlib-update-dependencies' &&
863877 steps.get-label-actor.outputs.username != 'mathlib-splicebot'
864878 name: check team membership
865- uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3 .0.0
879+ uses: tspascoal/get-user-teams-membership@818140d631d5f29f26b151afbe4179f87d9ceb5e # v4 .0.1
866880 id: actorTeams
867881 with:
868882 organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
0 commit comments