Merge branch 'master' into continuousLinearEquiv_ofContinuousLinear

Author: TJHeeringa

.git-blame-ignore-revs

@@ -4,3 +4,5 @@
 fc48848e4374f13c796a7399bfccd2e228f776df
 # 2025-11-19 move Mathlib to the module system (#31786)
 6a54a80825b060ab20dc31751ebdce78b3a3b518
+# 2025-12-01 fix spelling in doc-strings (#32286)
+b728e1450a53133aa4171eeadc0bc8d3ee58415c

.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: 0cd6cbc879d9241f3b4f6cb7e8291e34128c5654
+    default: 5668fbbccf0fecefdfcddf539b8406db197dfc59
   path:
     description: Checkout destination path.
     required: false

.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:
@@ -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 }}

.github/workflows/build_template.yml

@@ -1,4 +1,5 @@
-# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, and ci_dev.yml.
+# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, ci_dev.yml,
+# and release_cache.yml.
 
 on:
   workflow_call:
@@ -686,12 +687,18 @@ jobs:
       # Sparse-checkout master's `.github/actions/` so the trust dispatch
       # below loads from a trust-rooted source, not from PR-branch-controlled
       # content. Mirrors the `Checkout local actions` step in the `build` job.
-      - name: Checkout local actions
+      # Also check out the cache tool (`Cache/`) at this ref. The verify step
+      # below compares it against the PR branch's `Cache/` to classify a cache
+      # 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
         with:
           ref: ${{ github.workflow_sha }}
           fetch-depth: 1
-          sparse-checkout: .github/actions
+          sparse-checkout: |
+            .github/actions
+            Cache
           path: workflow-actions
 
       # Sets MATHLIB_CACHE_FROM in env so the `cache get` calls below pick
@@ -730,16 +737,60 @@ jobs:
           lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get Archive Counterexamples
 
       - name: verify that everything was available in the cache
+        # Verify the cache reconstitutes this commit's oleans. This job reads
+        # the cache with the PR branch's own `lake exe cache get`. The write
+        # path uses master's `cache` binary for fork PRs and the PR branch's
+        # binary for every other build. So a fork PR whose `Cache/` differs
+        # from master reads a different `.ltar` key space (say, after a
+        # `rootHashGeneration` bump) and misses every file. That is an expected
+        # invalidation: warn and continue. Any other build reads and writes
+        # with the same binary, so a miss there is a real gap and is fatal.
+        env:
+          # GitHub sets this from the event payload; it is empty for pushes
+          # (master, bors), so those fail closed below.
+          HEAD_REPO_IS_FORK: ${{ github.event.pull_request.head.repo.fork }}
         run: |
-          echo "::group::{verify Mathlib cache}"
-          lake build --no-build --rehash -v Mathlib
-          echo "::endgroup::"
-          echo "::group::{verify Archive cache}"
-          lake build --no-build --rehash -v Archive
-          echo "::endgroup::"
-          echo "::group::{verify Counterexamples cache}"
-          lake build --no-build --rehash -v Counterexamples
-          echo "::endgroup::"
+          set +e
+          fail=0
+          for target in Mathlib Archive Counterexamples; do
+            echo "::group::{verify ${target} cache}"
+            lake build --no-build --rehash -v "${target}" || fail=1
+            echo "::endgroup::"
+          done
+          if [ "${fail}" -eq 0 ]; then
+            exit 0
+          fi
+
+          # Only fork PRs read and write the cache with different binaries.
+          # Every other build (master, bors, dev branches) uses one binary, so
+          # a miss is a real gap.
+          if [ "${HEAD_REPO_IS_FORK}" != "true" ]; then
+            echo "::error::Cache verification failed on an in-repo build; the uploaded cache is incomplete."
+            exit 1
+          fi
+
+          # `workflow-actions/Cache` is master's cache tool at
+          # `github.workflow_sha`; `Cache` is the PR branch's. Matching source
+          # means the key spaces agree, so the miss is a real gap. Differing
+          # source means the PR changed the key space, so the miss is expected.
+          # The cache writer is master's binary at upload time, which can be
+          # newer than `workflow_sha` when a `Cache/` change lands on master
+          # mid-build; that skew can only hard-fail like an unguarded verify
+          # or soft-pass a key space that genuinely diverged.
+          dout=$(diff -rq workflow-actions/Cache Cache 2>&1)
+          dstat=$?
+          if [ "${dstat}" -eq 0 ]; then
+            echo "::error::Cache verification failed and this PR's Cache/ matches master's, so the key spaces agree: the uploaded cache is incomplete."
+            exit 1
+          elif [ "${dstat}" -eq 1 ]; then
+            echo "::warning::Cache verification incomplete, but this PR's Cache/ differs from master's. CI wrote the cache with master's binary and this job reads it with the PR branch's, so a changed key space (such as a rootHashGeneration bump) misses as expected. Continuing; the cache repopulates once this lands on master."
+            echo "${dout}"
+            exit 0
+          else
+            echo "::error::Cache verification failed and master's Cache/ baseline could not be compared (diff status ${dstat}); treating as a failure."
+            echo "${dout}"
+            exit 1
+          fi
 
       - name: check declarations in db files
         run: |

.github/workflows/release_cache.yml

@@ -0,0 +1,103 @@
+name: publish release cache
+
+# Publishes the Mathlib cache for release tags whose commits are not on
+# `master`.
+#
+# Patch releases (`v4.X.Y` with Y ≥ 1) and patched release candidates (e.g.
+# `v4.32.0-rc1-patch1`) are committed on `bump_to_*` branches that never merge
+# back into `master`, so the master push build never caches them; their branch
+# CI writes only the fork-trust container, which a canonical checkout at the
+# tag never reads. This workflow rebuilds the tagged commit and publishes the
+# result to the `master` container, where every consumer finds it. Tags that
+# point at commits on `master` (plain release candidates and `.0` releases)
+# are already cached by the master push build, so the gate job skips them.
+#
+# Trust model:
+#   - Creating a `v4.*` tag is restricted to release managers by a tag
+#     ruleset, so a tag push is a deliberate release-manager action — and the
+#     tagged tree is what runs here, including this workflow file. Tags cut
+#     from lineages predating this file simply never trigger it.
+#   - The upload job mints its OIDC token under the `cache-upload-master`
+#     environment (inside build_template.yml); the environment's deployment
+#     policy admits only `master`, `staging`, and `v4.*` tag refs.
+#
+# Retry: a spuriously failed run can simply be re-run ("Re-run failed jobs" /
+# `gh run rerun`) — same tag, same tree, no tag re-push involved. The
+# `workflow_dispatch` trigger covers what re-run cannot: a tag push that never
+# produced a run, or a re-run window that has expired. Dispatch it AT the tag
+# ref (`gh workflow run release_cache.yml --ref v4.X.Y`); the run then executes
+# the tag's own tree exactly as a tag push would.
+
+on:
+  push:
+    tags:
+      - 'v4.*'
+  # Manual fallback; see the retry note above. The `tags` filter does not
+  # apply to dispatches — the gate job's ref guards enforce it instead, so a
+  # dispatch on a branch ref skips cleanly.
+  workflow_dispatch:
+
+# `v4.*` tags are immutable (the tag ruleset blocks updates), so this group
+# only ever collides on re-runs of the same tag; keep those queued rather
+# than cancelled.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+
+# Read-only by default; the build job elevates for itself only.
+permissions:
+  contents: read
+
+jobs:
+  gate:
+    name: skip tags already on master
+    # The ref guards double as the dispatch-path filter; on the push path the
+    # `tags` trigger filter has already enforced them.
+    if: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref_type == 'tag' && startsWith(github.ref_name, 'v4.') }}
+    runs-on: ubuntu-latest
+    outputs:
+      off_master: ${{ steps.check.outputs.off_master }}
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        with:
+          # `merge-base` needs history, so fetch all of it.
+          fetch-depth: 0
+
+      - name: check whether the tagged commit is on master
+        id: check
+        run: |
+          if git merge-base --is-ancestor "$GITHUB_SHA" origin/master; then
+            echo "Tag $GITHUB_REF_NAME points at a commit on master; the master push build covers its cache."
+            echo "off_master=false" >> "$GITHUB_OUTPUT"
+          else
+            echo "Tag $GITHUB_REF_NAME is not on master; rebuilding it to publish its cache."
+            echo "off_master=true" >> "$GITHUB_OUTPUT"
+          fi
+
+  build:
+    name: ci
+    needs: gate
+    if: ${{ needs.gate.outputs.off_master == 'true' }}
+    # What build_template.yml needs, granted to this job only — the same set
+    # build.yml grants it on push events. In particular, the OIDC token for
+    # the cache upload can be minted here and nowhere else in this workflow.
+    permissions:
+      contents: read
+      id-token: write
+      actions: read  # Allow get-tools to download the prebuilt tools artifact from master's publish_tools runs
+      pull-requests: write  # Only allow PR comments/labels
+    uses: ./.github/workflows/build_template.yml
+    with:
+      concurrency_group: ${{ github.workflow }}-${{ github.ref }}
+      pr_branch_ref: ${{ github.sha }}
+      # Release tags publish to the `master` container under the master writer
+      # identity; see the trust note above and cache-trust-dispatch, which
+      # routes `v4.*` tag refs to that container.
+      cache_application_id: ${{ vars.CACHE_MASTER_WRITER_AZURE_APP_ID }}
+      cache_environment: cache-upload-master
+      # The cache-snapshot warming artifact exists to seed master and PR
+      # builds, which a release tag's snapshot cannot do.
+      publish_cache: false
+      # Skip the Post-CI job: it grooms PR labels, and a tag run has no PR.
+      run_post_ci: false
+      runs_on: pr
+    secrets: inherit