@@ -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
@@ -725,17 +733,42 @@ jobs:
725733 run : |
726734 lake exe graph
727735
736+ name : Checkout local actions
737+ uses : actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
738+ with :
739+ ref : ${{ github.workflow_sha }}
740+ fetch-depth : 1
741+ sparse-checkout : .github/actions
742+ path : workflow-actions
743+
744+ - name : Get mathlib-ci
745+ uses : ./workflow-actions/.github/actions/get-mathlib-ci
746+
747+ - name : dump declarations and transitive-import counts
748+ run : |
749+ lake env lean --run "${CI_SCRIPTS_DIR}/pr_summary/dumpReasonableDecls.lean" \
750+ --out decls.txt --imports-out imports.json Mathlib
751+
728752name : upload the import graph
729- uses : actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
753+ uses : actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
730754 with :
731755 name : import-graph
732- path : import_graph.dot
733- # # the default is 90, but we build often, so unless there's a reason
734- # # to care about old copies in the future, just say 7 days for now
735- retention-days : 7
756+ path : |
757+ import_graph.dot
758+ decls.txt
759+ imports.json
760+ # # Master pushes: 90 days, so later PRs forked from these commits
761+ # # can consume the dumps from the artifact. Other branches: 7 days.
762+ retention-days : ${{ github.ref == 'refs/heads/master' && '90' || '7' }}
736763
737764 - name : clean up the import graph file
738- run : rm import_graph.dot
765+ run : rm -f import_graph.dot decls.txt imports.json
766+
767+ - name : check all scripts build successfully
768+ run : |
769+ lake env lean scripts/create_deprecated_modules.lean
770+ lake env lean scripts/autolabel.lean
771+ lake exe check_title_labels --labels "t-algebra" "feat: dummy PR for testing"
739772
740773name : build everything
741774 # make sure everything is available for test/import_all.lean
@@ -862,7 +895,7 @@ jobs:
862895 steps.get-label-actor.outputs.username != 'mathlib-update-dependencies' &&
863896 steps.get-label-actor.outputs.username != 'mathlib-splicebot'
864897 name: check team membership
865- uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3 .0.0
898+ uses: tspascoal/get-user-teams-membership@818140d631d5f29f26b151afbe4179f87d9ceb5e # v4 .0.1
866899 id: actorTeams
867900 with:
868901 organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
0 commit comments