Update lean-toolchain for leanprover/lean4#14595

Author: leanprover-community-mathlib4-bot

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 5668fbbccf0fecefdfcddf539b8406db197dfc59
+    default: 2ad9371b8b135fc702e135e4e91ddace151e549d
   path:
     description: Checkout destination path.
     required: false

.github/workflows/PR_summary.yml

@@ -17,7 +17,7 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0
@@ -29,7 +29,7 @@ jobs:
         allow-unsafe-pr-checkout: true
 
     - name: Checkout local actions
-      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       with:
         ref: ${{ github.workflow_sha }}
         fetch-depth: 1
@@ -67,7 +67,7 @@ jobs:
         fi
 
     - name: Set up Python
-      uses: actions/setup-python@ece7cb06caefa5fff74198d8649806c4678c61a1 # v6.3.0
+      uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
       with:
         python-version: 3.12
 
@@ -220,12 +220,23 @@ jobs:
         else
           declDiff="$(printf '#### Declarations diff (regex)\n\n%s\n' "${declDiff}")"
         fi
-        # Append a placeholder for the post-build, Lean-aware diff. The
-        # `decls-diff.yml` workflow replaces the region between the markers (see
-        # mathlib-ci's `updateDeclsDiffSection.py`); the regex block above is left
-        # as-is. The markers are HTML comments (invisible when rendered), and the
-        # heading carries the status (`pending` → `(Lean)` / `(Lean -- unavailable)`).
-        declDiff="$(printf '%s\n\n<!-- DECLS_DIFF_LEAN_BEGIN -->\n#### Declarations diff (Lean -- pending)\n\n_Computed after the build finishes._\n<!-- DECLS_DIFF_LEAN_END -->\n' "${declDiff}")"
+        # Append the post-build, Lean-aware diff region. The `decls-diff.yml`
+        # workflow later replaces the content between the markers (see mathlib-ci's
+        # `updateDeclsDiffSection.py`); the regex block above is left as-is. The
+        # markers are HTML comments (invisible when rendered), and the heading
+        # carries the status (`pending` → `(Lean)` / `(Lean -- unavailable)`).
+        #
+        # Because this pre-build step rewrites the whole comment, it would otherwise
+        # blank a previously-shown diff back to `pending` on every push. Instead we
+        # ask `updateDeclsDiffSection.py` (MODE=emit) to carry the existing real diff
+        # forward — relabelled stale — so it stays visible until the new build lands;
+        # on the first run (or with no prior diff) it prints the pending placeholder.
+        leanRegion="$(MODE=emit \
+          NEW_HEADING='#### Declarations diff (Lean -- stale, waiting for the new build)' \
+          REPO="${{ github.repository }}" PR_NUMBER="${PR}" PR_HEAD_SHA="${currentHash}" \
+          python3 "${CI_SCRIPTS_DIR}/pr_summary/updateDeclsDiffSection.py" \
+          || printf '#### Declarations diff (Lean -- pending)\n\n_Computed after the build finishes._')"
+        declDiff="$(printf '%s\n\n<!-- DECLS_DIFF_LEAN_BEGIN -->\n%s\n<!-- DECLS_DIFF_LEAN_END -->\n' "${declDiff}" "${leanRegion}")"
         git checkout "${currentHash}" --
         hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
         printf 'hashURL: %s' "${hashURL}"

.github/workflows/actionlint.yml

@@ -9,10 +9,10 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
       - name: suggester / actionlint
-        uses: reviewdog/action-actionlint@6fb7acc99f4a1008869fa8a0f09cfca740837d9d # v1.72.0
+        uses: reviewdog/action-actionlint@50842263c20a7c46bd0065b9e624d3c569db061e # v1.73.0
         with:
           tool_name: actionlint
           fail_level: any
@@ -21,7 +21,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
       # Using our fork's PR branch until upstream merges the improved error reporting:
       # https://github.com/zgosalvez/github-actions-ensure-sha-pinned-actions/pull/288

.github/workflows/add_label_from_diff.yaml

@@ -18,7 +18,7 @@ jobs:
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
     - name: Checkout master branch to build autolabel from
-      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       with:
         ref: master
         path: tools
@@ -34,7 +34,7 @@ jobs:
       run: |
         lake build autolabel
     - name: Checkout branch to label
-      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       with:
         ref: ${{ github.event.pull_request.head.sha || github.sha }}
         fetch-depth: 0

.github/workflows/build_template.yml

@@ -48,6 +48,7 @@ env:
   # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
+  MATHLIB_CACHE_BASE_URL: ${{ vars.MATHLIB_CACHE_BASE_URL }}
 
 jobs:
   build:
@@ -57,6 +58,7 @@ jobs:
       build-outcome: ${{ steps.build.outcome }}
       archive-outcome: ${{ steps.archive.outcome }}
       counterexamples-outcome: ${{ steps.counterexamples.outcome }}
+      wanted-outcome: ${{ steps.wanted.outcome }}
       cache-staging-has-files: ${{ steps.cache_staging_check.outputs.has_files }}
       mk_all-outcome: ${{ steps.mk_all.outcome }}
       noisy-outcome: ${{ steps.noisy.outcome }}
@@ -80,7 +82,7 @@ jobs:
           # We just populate the env vars for this step to make them viewable in the logs
 
       - name: Checkout local actions
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1
@@ -230,12 +232,13 @@ jobs:
       # storing and transferring oleans over the network.
       # Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
 
-      - name: fetch archive and counterexamples cache
+      - name: fetch archive, counterexamples and wanted cache
         shell: bash
         run: |
           cd pr-branch
           ../tools-branch/.lake/build/bin/cache get Archive.lean
           ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
+          ../tools-branch/.lake/build/bin/cache get Wanted.lean
 
       - name: build archive
         id: archive
@@ -253,8 +256,16 @@ jobs:
           ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
           # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
+      - name: build wanted
+        id: wanted
+        continue-on-error: true
+        run: |
+          cd pr-branch
+          ../tools-branch/scripts/lake-build-with-retry.sh Wanted
+          # results of build at pr-branch/.lake/build_summary_Wanted.json
+
       # Runs in the build job because it only needs the freshly-built Mathlib/
-      # Archive/Counterexamples oleans, which are present here; keeping it in
+      # Archive/Counterexamples/Wanted oleans, which are present here; keeping it in
       # `build` also spares `test_lint` from fetching Archive/Counterexamples.
       - name: check for noisy stdout lines
         id: noisy
@@ -263,7 +274,7 @@ jobs:
           buildMsgs="$(
             ##  we exploit `lake`s replay feature: since the cache is present, running
             ##  `lake build` will reproduce all the outputs without having to recompute
-            lake build -q --iofail Mathlib Archive Counterexamples
+            lake build -q --iofail Mathlib Archive Counterexamples Wanted
           )"
           if [ -n "${buildMsgs}" ]
           then
@@ -300,6 +311,13 @@ jobs:
           cd pr-branch
           lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Counterexamples.lean
 
+      - name: stage Wanted cache files
+        if: ${{ steps.wanted.outcome == 'success' }}
+        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
+        run: |
+          cd pr-branch
+          lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Wanted.lean
+
       - name: check cache staging contents
         id: cache_staging_check
         if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
@@ -395,7 +413,7 @@ jobs:
         shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
     steps:
       - name: Checkout local actions
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1
@@ -463,19 +481,19 @@ jobs:
       # the archive/counterexamples builds all succeeded. The condition reads those
       # from the build job's outputs, and the problem-matcher wrap is gated to match.
       - name: begin gh-problem-match-wrap for test step
-        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
+        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' && needs.build.outputs.wanted-outcome == 'success' }}
         uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
         with:
           action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
           linters: lean
       - name: test mathlib
-        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
+        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' && needs.build.outputs.wanted-outcome == 'success' }}
         id: test
         run: |
           cd pr-branch
           ../tools-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test
       - name: end gh-problem-match-wrap for test step
-        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
+        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' && needs.build.outputs.wanted-outcome == 'success' }}
         uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
         with:
           action: remove
@@ -605,7 +623,7 @@ jobs:
       # `build_template` via `pull_request_target`, never this one — so
       # `pr_branch_ref` is always a trusted ref here. Fork PRs keep `master`.
       - name: Checkout tools branch
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.event.pull_request.head.repo.fork && 'master' || inputs.pr_branch_ref) }}
           fetch-depth: 1
@@ -675,7 +693,7 @@ jobs:
       contents: read
     steps:
 
-      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: ${{ inputs.pr_branch_ref }}
           # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
@@ -692,7 +710,7 @@ jobs:
       # miss. `github.workflow_sha` is the base ref the workflow runs from,
       # master for fork PRs, whose `cache` binary wrote the cache.
       - name: Checkout local actions and Cache baseline
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1
@@ -802,7 +820,7 @@ jobs:
           lake exe graph
 
       - name: Checkout local actions
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1
@@ -1015,7 +1033,7 @@ jobs:
             contains(steps.actorTeams.outputs.teams, 'bot-users')
           )
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
-        uses: GrantBirki/comment@3439715f0cf3b8fc29bf47be0e3226679c06c41a # v3.0.0
+        uses: GrantBirki/comment@937820f3623fd0e300294bcc64ac7577fc0ad4cc # v3.0.3
         with:
           # This token is masked by the token minting action and will not be logged accidentally.
           token: ${{ steps.auto-merge-app-token.outputs.token }}

.github/workflows/cache_test.yml

@@ -41,7 +41,7 @@ jobs:
       run:
         shell: bash
     steps:
-      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
       # Install elan and the toolchain cross-platform. Build/test/lint, the
       # Mathlib cache, and the GitHub cache are all disabled, so this is a

.github/workflows/check_pr_titles.yaml

@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: master
       - name: Configure Lean
@@ -70,7 +70,7 @@ jobs:
           fi
 
       - name: Add comment to fix PR title
-        uses: marocchino/sticky-pull-request-comment@0ea0beb66eb9baf113663a64ec522f60e49231c0 # v3.0.4
+        uses: marocchino/sticky-pull-request-comment@5770ad5eb8f42dd2c4f34da00c94c5381e49af88 # v3.0.5
         if: failure() && steps.pr-title-check.outputs.errors
         with:
           header: 'PR Title Check'
@@ -120,7 +120,7 @@ jobs:
 
       - name: Add comment that PR title is fixed
         if: steps.pr-title-check.outcome == 'success'
-        uses: marocchino/sticky-pull-request-comment@0ea0beb66eb9baf113663a64ec522f60e49231c0 # v3.0.4
+        uses: marocchino/sticky-pull-request-comment@5770ad5eb8f42dd2c4f34da00c94c5381e49af88 # v3.0.5
         with:
           header: 'PR Title Check'
           # should do nothing if a 'PR Title Check' comment does not exist

.github/workflows/commit_verification.yml

@@ -33,14 +33,14 @@ jobs:
     # This is a quick check to avoid unnecessary runs
     steps:
       - name: Checkout PR head
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           # Checkout the actual PR head, not the merge commit GitHub creates
           ref: ${{ github.event.pull_request.head.sha }}
           # Fetch full history to access all PR commits
           fetch-depth: 0
       - name: Checkout local actions
-        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1

.github/workflows/daily-master-tag.yml

@@ -14,7 +14,7 @@ jobs:
     runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
-      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: master