Merge branch 'master' into greens-relations-defs

Author: ReemMelamed

.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: 194b03113712fdf55c2c29651f161893f0305fe8
+    default: 4db29a340d585b5ca9cc45ba5b951a3939753d53
   path:
     description: Checkout destination path.
     required: false

.github/workflows/PR_summary.yml

@@ -17,14 +17,16 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0
         path: pr-branch
+        # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+        persist-credentials: false
 
     - name: Checkout local actions
-      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
       with:
         ref: ${{ github.workflow_sha }}
         fetch-depth: 1
@@ -211,10 +213,16 @@ jobs:
         declDiff=$("${CI_SCRIPTS_DIR}/pr_summary/declarations_diff.sh")
         if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ]
         then
-          declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")"
+          declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff (regex)" "${declDiff}")"
         else
-          declDiff="$(printf '#### Declarations diff\n\n%s\n' "${declDiff}")"
+          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}")"
         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,7 +9,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
 
       - name: suggester / actionlint
         uses: reviewdog/action-actionlint@6fb7acc99f4a1008869fa8a0f09cfca740837d9d # v1.72.0
@@ -21,7 +21,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
 
       # 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

@@ -22,7 +22,7 @@ jobs:
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
     - name: Checkout master branch to build autolabel from
-      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
       with:
         ref: master
         path: tools
@@ -38,11 +38,13 @@ jobs:
       run: |
         lake build autolabel
     - name: Checkout branch to label
-      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
       with:
         ref: ${{ github.event.pull_request.head.sha || github.sha }}
         fetch-depth: 0
         path: pr-branch
+        # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+        persist-credentials: false
     - name: Run autolabel
       working-directory: pr-branch
       run: |

.github/workflows/bors.yml

@@ -30,6 +30,10 @@ jobs:
       # Use the MASTER cache key only when merging into mathlib4 (staging branch);
       # 'bors try' runs (trying branch) and nightly-testing use NON_MASTER
       cache_application_id: ${{ github.ref_name == 'staging' && github.repository == 'leanprover-community/mathlib4' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
+      # Track the cache_application_id choice above; the environment fixes the OIDC subject the Azure app trusts.
+      # nightly-testing is intentionally left without an environment ('') so it keeps its existing ref-based trust.
+      # TODO: give mathlib4-nightly-testing its own cache-upload environment + federated credential.
+      cache_environment: ${{ github.repository == 'leanprover-community/mathlib4' && (github.ref_name == 'staging' && 'cache-upload-master' || 'cache-upload-forks') || '' }}
       # bors runs should build the tools from their commit-under-test: after all, we are trying to
       # test 'what would happen if this was merged', so we need to use the 'would-be-post-merge' tools
       tools_branch_ref: ${{ github.sha }}

.github/workflows/bot_fix_style.yaml

@@ -12,6 +12,14 @@ on:
     # triggers on a review comment
     types: [created, edited]
 
+# `lint-style-action` in `fix` mode pushes a style-fix commit and reacts/comments
+# on the PR. Grant exactly those scopes rather than inheriting the default token
+# permissions; all other scopes are implicitly 'none'.
+permissions:
+  contents: write       # push the style-fix commit to the PR branch
+  pull-requests: write  # add the bot's reaction/comment
+  issues: write         # PR comment reactions go through the issues API
+
 jobs:
   fix_style:
     # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not

.github/workflows/build.yml

@@ -37,5 +37,9 @@ jobs:
       pr_branch_ref: ${{ github.sha }}
       # Use the MASTER cache key only on mathlib4/master; nightly-testing and other branches use NON_MASTER
       cache_application_id: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref == 'refs/heads/master' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
+      # Track the cache_application_id choice above; the environment fixes the OIDC subject the Azure app trusts.
+      # nightly-testing is intentionally left without an environment ('') so it keeps its existing ref-based trust.
+      # TODO: give mathlib4-nightly-testing its own cache-upload environment + federated credential.
+      cache_environment: ${{ github.repository == 'leanprover-community/mathlib4' && (github.ref == 'refs/heads/master' && 'cache-upload-master' || 'cache-upload-forks') || '' }}
       runs_on: pr
     secrets: inherit

.github/workflows/build_fork.yml

@@ -37,5 +37,6 @@ jobs:
       concurrency_group: ${{ github.workflow }}-${{ github.event.pull_request.number }}
       pr_branch_ref: ${{ github.event.pull_request.head.sha }}
       cache_application_id: ${{ vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
+      cache_environment: cache-upload-forks
       runs_on: pr
     secrets: inherit

.github/workflows/build_template.yml

@@ -27,6 +27,12 @@ on:
       cache_application_id:
         type: string
         required: true
+      cache_environment:
+        # GitHub environment for the `upload_cache` job. Its only role is to fix the
+        # OIDC `sub` claim to `...:environment:<name>`, which the Azure cache app's
+        # federated credential is scoped to; it must match the writer `cache_application_id`.
+        type: string
+        required: true
 
 env:
   # Disable Lake's automatic fetching of cloud builds.
@@ -89,7 +95,7 @@ jobs:
 
       # Checkout a trusted branch to build the tooling from
       - name: Checkout tools branch
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
           # we don't maintain a `master` branch at all.
@@ -99,7 +105,7 @@ jobs:
           path: tools-branch
 
       - name: Checkout local actions
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1
@@ -122,11 +128,14 @@ jobs:
 
       # Checkout the PR branch into a subdirectory
       - name: Checkout PR branch
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           ref: ${{ inputs.pr_branch_ref }}
           fetch-depth: 2 # we may fetch cache from the commit before this one (or earlier)
           path: pr-branch
+          # This is an untrusted (potentially fork) checkout whose code we build.
+          # Don't leave the GITHUB_TOKEN in pr-branch/.git/config, where that code could read it.
+          persist-credentials: false
 
       - name: Prepare DownstreamTest directory
         shell: bash
@@ -513,19 +522,19 @@ jobs:
         run: |
           cd pr-branch
           set -o pipefail
-          # Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
+          # If lint fails because the PR predates lake-lint configuration or the
+          # old --trace argument-parsing behavior, ask the author to merge master.
           # We use .lake/ for the output file because landrun restricts /tmp access
           for attempt in 1 2; do
-            if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
+            if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake lint -- --trace 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
               break
             fi
             status=${PIPESTATUS[0]}
-            if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
+            if grep -qE "cannot parse arguments|no lint driver configured" ".lake/lint_output_attempt_${attempt}.txt"; then
               echo ""
               echo "=============================================================================="
-              echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
-              echo "the --trace flag. Please merge 'master' into your PR branch to get the"
-              echo "updated linter, then push again."
+              echo "ERROR: Your branch predates the current 'lake lint' configuration."
+              echo "Please merge 'master' into your PR branch and push again."
               echo ""
               echo "You can do this with:"
               echo "  git fetch upstream"
@@ -574,7 +583,7 @@ jobs:
       - name: Generate lean-pr-testing app token
         if: ${{ always() && github.repository == 'leanprover-community/mathlib4-nightly-testing' && (startsWith(github.ref_name, 'lean-pr-testing-') || startsWith(github.ref_name, 'batteries-pr-testing-')) }}
         id: lean-pr-testing-token
-        uses: actions/create-github-app-token@1b10c78c7865c340bc4f6099eb2f838309f1e8c3 # v3.1.1
+        uses: actions/create-github-app-token@bcd2ba49218906704ab6c1aa796996da409d3eb1 # v3.2.0
         with:
           # `batteries-pr-testing-*` branches need a token scoped to `leanprover-community/batteries`
           # for the labelling API; `lean-pr-testing-*` branches need one scoped to `leanprover/lean4`.
@@ -605,6 +614,10 @@ jobs:
     name: Upload to cache
     needs: [build]
     runs-on: ubuntu-latest # These steps run on a GitHub runner; no landrun sandboxing is needed.
+    # Pins the OIDC `sub` claim to `...:environment:<cache_environment>`, which the Azure cache
+    # app's federated credential is scoped to. A token minted by any job without this environment
+    # (e.g. the untrusted build/post_steps/style_lint jobs) cannot satisfy that trust.
+    environment: ${{ inputs.cache_environment }}
     permissions:
       contents: read
       id-token: write
@@ -614,7 +627,7 @@ jobs:
     if: ${{ always() && needs.build.outputs.cache-staging-has-files == 'true' }}
     steps:
       - name: Checkout tools branch
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
           fetch-depth: 1
@@ -684,11 +697,17 @@ jobs:
     needs: [build, upload_cache]
     if: ${{ always() && needs.build.result == 'success' && (needs.upload_cache.result == 'success' || needs.upload_cache.result == 'skipped') }}
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
+    # This job checks out and executes (potentially fork) PR code unsandboxed,
+    # so it must not inherit any write-capable token.
+    permissions:
+      contents: read
     steps:
 
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           ref: ${{ inputs.pr_branch_ref }}
+          # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+          persist-credentials: false
 
       - name: Configure Lean
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
@@ -734,7 +753,7 @@ jobs:
           lake exe graph
 
       - name: Checkout local actions
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1
@@ -748,6 +767,21 @@ jobs:
         run: |
           lake env lean --run "${CI_SCRIPTS_DIR}/pr_summary/dumpReasonableDecls.lean" \
             --out decls.txt --imports-out imports.json Mathlib
+          ## Record the PR number so the post-build `decls-diff` workflow can find
+          ## the comment to patch without the (laggy) commit-SHA search API. Empty
+          ## for non-PR builds (push to master / bors); the consumer then falls
+          ## back to the commit's associated PRs.
+          printf '%s' "${{ github.event.pull_request.number }}" > pr_number.txt
+
+      - name: ensure dump outputs are regular files
+        run: |
+          for f in decls.txt imports.json import_graph.dot pr_number.txt; do
+            if [ -L "$f" ] || [ ! -f "$f" ]; then
+              echo "Refusing to upload: $f is not a regular file." >&2
+              ls -la -- "$f" >&2 || true
+              exit 1
+            fi
+          done
 
       - name: upload the import graph
         uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
@@ -757,12 +791,13 @@ jobs:
             import_graph.dot
             decls.txt
             imports.json
+            pr_number.txt
           ## Master pushes: 90 days, so later PRs forked from these commits
           ## can consume the dumps from the artifact. Other branches: 7 days.
           retention-days: ${{ github.ref == 'refs/heads/master' && '90' || '7' }}
 
       - name: clean up the import graph file
-        run: rm -f import_graph.dot decls.txt imports.json
+        run: rm -f import_graph.dot decls.txt imports.json pr_number.txt
 
       - name: check all scripts build successfully
         run: |
@@ -788,6 +823,10 @@ jobs:
   style_lint:
     name: Lint style
     runs-on: ubuntu-latest
+    # This job lints (potentially fork) PR code, so it must not inherit any write-capable token.
+    # In `check` mode lint-style-action only reads and validates code locally (no API calls).
+    permissions:
+      contents: read
     steps:
       - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
         with:
@@ -895,7 +934,7 @@ jobs:
           steps.get-label-actor.outputs.username != 'mathlib-update-dependencies' &&
           steps.get-label-actor.outputs.username != 'mathlib-splicebot'
         name: check team membership
-        uses: tspascoal/get-user-teams-membership@818140d631d5f29f26b151afbe4179f87d9ceb5e # v4.0.1
+        uses: tspascoal/get-user-teams-membership@b2546c5affc730fd8e3d8483ae9ad3621938c2f9 # v4.0.2
         id: actorTeams
         with:
           organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
@@ -914,7 +953,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@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
+        uses: GrantBirki/comment@3439715f0cf3b8fc29bf47be0e3226679c06c41a # v3.0.0
         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/check_pr_titles.yaml

@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           ref: master
       - name: Configure Lean