Merge branch 'master' into h1connected

Author: CoolRmal

.github/actions/cache-trust-dispatch/action.yml

@@ -1,4 +1,4 @@
-# Single source of truth mapping (repo, branch) → (upload container,
+# Single source of truth mapping (repo, ref) → (upload container,
 # read fallback chain) for Mathlib's multi-container cache.
 #
 # Called by build, upload_cache, and post_steps in build_template.yml so
@@ -14,7 +14,10 @@ inputs:
     description: GitHub repo full name (`owner/name`).
     required: true
   branch:
-    description: Branch name (`github.head_ref || github.ref_name`).
+    description: |
+      Branch name (`github.head_ref || github.ref_name`); on tag-triggered
+      runs this is the tag name, distinguished via `github.ref_type` inside
+      the dispatch step.
     required: true
   head-sha:
     description: |
@@ -55,6 +58,10 @@ runs:
         REPO="${{ inputs.repo }}"
         BRANCH="${{ inputs.branch }}"
         HEAD_SHA="${{ inputs.head-sha }}"
+        # Whether `branch` names a branch or a tag. Read from the run context
+        # rather than an input: unlike `repo`/`branch`, the value does not
+        # depend on which event shape (PR vs push) the caller handles.
+        REF_TYPE="${{ github.ref_type }}"
         PRIMARY=""
         READ_CHAIN=""
         REPO_SCOPE=""
@@ -80,30 +87,55 @@ runs:
         else
         case "$REPO" in
           "leanprover-community/mathlib4")
-            case "$BRANCH" in
-              "master"|"staging")
-                # Master / staging are the only writers that feed `master`
-                # (`staging` is bors's merge candidate, which fast-forwards to
-                # `master`). Read `master` only, not the default [master,
-                # legacy]: files the read chain serves are skipped at stage
-                # time, so keeping `legacy` would leave legacy-only files out of
-                # `master` for good. Reading `master` alone turns them into
-                # misses that get rebuilt and uploaded, so `master` fills itself
-                # into a standalone cache. (Only PRIMARY=master does this; other
-                # runs write to `forks` and keep the wider chain.)
-                PRIMARY="master"
-                READ_CHAIN="master"
-                ;;
-              *)
-                # `bors trying`, `ci-dev/*`, maintainer dev branches on the
-                # canonical repo: trust level is fork-equivalent (the OIDC
-                # token's RBAC scopes them to `forks`). Reads must widen
-                # past the default [master, legacy] so the post-build
-                # verification finds the just-uploaded fork-trust artifacts.
-                PRIMARY="forks"
-                READ_CHAIN="master,forks,legacy"
-                ;;
-            esac
+            if [ "$REF_TYPE" = "tag" ]; then
+              case "$BRANCH" in
+                v4.*)
+                  # `v4.*` release tags: release_cache.yml rebuilds off-master
+                  # release commits (patch releases, patched release
+                  # candidates) and publishes them into `master`, the container
+                  # canonical checkouts read. Tag creation is restricted to
+                  # release managers by a tag ruleset, and the
+                  # `cache-upload-master` environment admits `v4.*` tag refs,
+                  # so these builds carry master trust. Reads are `master`-only
+                  # for the same fill-in reason as the master/staging arm
+                  # below.
+                  PRIMARY="master"
+                  READ_CHAIN="master"
+                  ;;
+                *)
+                  # Other tags have no trust class of their own:
+                  # fork-equivalent, like the dev-branch arm below.
+                  PRIMARY="forks"
+                  READ_CHAIN="master,forks,legacy"
+                  ;;
+              esac
+            else
+              case "$BRANCH" in
+                "master"|"staging")
+                  # Master, staging, and `v4.*` release tags (above) are the
+                  # only writers that feed `master` (`staging` is bors's merge
+                  # candidate, which fast-forwards to `master`). Read `master`
+                  # only, not the default [master, legacy]: files the read
+                  # chain serves are skipped at stage time, so keeping `legacy`
+                  # would leave legacy-only files out of `master` for good.
+                  # Reading `master` alone turns them into misses that get
+                  # rebuilt and uploaded, so `master` fills itself into a
+                  # standalone cache. (Only PRIMARY=master does this; other
+                  # runs write to `forks` and keep the wider chain.)
+                  PRIMARY="master"
+                  READ_CHAIN="master"
+                  ;;
+                *)
+                  # `bors trying`, `ci-dev/*`, maintainer dev branches on the
+                  # canonical repo: trust level is fork-equivalent (the OIDC
+                  # token's RBAC scopes them to `forks`). Reads must widen
+                  # past the default [master, legacy] so the post-build
+                  # verification finds the just-uploaded fork-trust artifacts.
+                  PRIMARY="forks"
+                  READ_CHAIN="master,forks,legacy"
+                  ;;
+              esac
+            fi
             ;;
           "leanprover-community/mathlib4-nightly-testing")
             case "$BRANCH" in

.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: 57c68e7faac5aea96e58a94ca4a334a1999f0d31
   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

@@ -3,10 +3,6 @@ name: Autolabel PRs
 on:
   pull_request_target:
     types: [opened]
-  push:
-    paths:
-      - scripts/autolabel.lean
-      - .github/workflows/add_label_from_diff.yaml
 
 # Limit permissions for GITHUB_TOKEN for the entire workflow
 permissions:
@@ -22,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
@@ -38,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
@@ -51,31 +47,7 @@ jobs:
     - name: Run autolabel
       working-directory: pr-branch
       run: |
-        labels="$("${GITHUB_WORKSPACE}/tools/.lake/build/bin/autolabel")"
-        printf '%s\n' "${labels}"
-        # extract
-        label="$(printf '%s' "${labels}" | sed -n 's=^::notice::.*#\[\([^,]*\)\].*=\1=p')"
-        printf 'label: "%s"\n' "${label}"
-        if [ -n "${label}" ] && [ -n "${PR_NUMBER}" ]
-        then
-          printf 'Applying label %s\n' "${label}"
-          # we use curl rather than octokit/request-action so that the job won't fail
-          # (and send an annoying email) if the labels don't exist
-          url="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/labels"
-          printf 'url: %s\n' "${url}"
-          jsonLabel="$(printf '{"labels":["%s"]}' "${label}")"
-          printf 'jsonLabel: %s\n' "${jsonLabel}"
-          curl --request POST \
-            --header 'Accept: application/vnd.github+json' \
-            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \
-            --header 'X-GitHub-Api-Version: 2022-11-28' \
-            --url "${url}" \
-            --data "${jsonLabel}"
-        else
-          echo "There is no single label that we could apply, so we are not applying any label."
-        fi
+        "${GITHUB_WORKSPACE}/tools/.lake/build/bin/autolabel" --pr "${{ github.event.pull_request.number }}" --curl "${{ secrets.GITHUB_TOKEN }}"
       env:
         GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        # the PR number could be undefined in workflows triggered by 'push',
-        # in which case we only log the applicable label and exit
         PR_NUMBER: ${{ github.event.pull_request.number }}