Merge branch 'master' into tb_ref9484

Author: tb65536

.github/workflows/PR_summary.yml

@@ -17,7 +17,7 @@ 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
@@ -26,7 +26,7 @@ jobs:
         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

.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,7 +38,7 @@ 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

.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/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,7 +128,7 @@ 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)
@@ -577,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`.
@@ -608,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
@@ -617,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
@@ -693,7 +703,7 @@ jobs:
       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.
@@ -743,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
@@ -908,7 +918,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 }}
@@ -927,7 +937,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

.github/workflows/ci_dev.yml

@@ -46,5 +46,6 @@ jobs:
       run_post_ci: ${{ inputs.run_post_ci }}
       mathlib_ci_ref: ${{ inputs.mathlib_ci_ref }}
       cache_application_id: ${{ vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
+      cache_environment: cache-upload-forks
       runs_on: pr
     secrets: inherit

.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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1