merge

Author: tb65536

.git-blame-ignore-revs

@@ -0,0 +1,8 @@
+# 2024-05-20 replace `refine'` with one underscore by `refine` (#13059)
+7493b5f81b4c031b87877c5c124bea1ddc4e567d
+# 2024-05-24 replace many `refine'` with `refine` (#13166)
+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=""
@@ -66,32 +73,69 @@ runs:
         # be 403'd by Azure regardless. The dispatch exists so the workflow
         # does the right thing in the honest case; defence in depth is RBAC.
 
+        # Privileged containers (master, nightly-testing, pr-toolchain-tests) are
+        # writable only by a repo's own native CI, whose OIDC token is RBAC-scoped
+        # to match. A cross-repo pull request is built by build_fork.yml with
+        # fork-trust credentials whatever repo the PR head lives on (e.g. a `bump/*`
+        # branch on the mathlib4-nightly-testing fork), so it can only write
+        # `forks`. `GITHUB_REPOSITORY` is the repo the workflow runs as (the base
+        # repo for `pull_request_target`), i.e. the one whose credentials this job
+        # holds; when it differs from `$REPO`, the build is a fork and targets
+        # `forks` regardless of the head repo's own trust class.
+        if [ "$REPO" != "$GITHUB_REPOSITORY" ]; then
+          PRIMARY="forks"
+        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
@@ -121,6 +165,7 @@ runs:
             PRIMARY="forks"
             ;;
         esac
+        fi
 
         # Per-commit cache namespace, only for fork-trust uploads. Closes the
         # within-fork temporal replay attack: each commit's CI run gets its

.github/actions/get-cache/action.yml

@@ -0,0 +1,115 @@
+# Get this commit's oleans, in two phases:
+#   1. Warm the cache from the `cache-snapshot` GitHub artifact (canonical repo only).
+#   2. Fetch this commit's oleans from the remote cache with the trusted master-built binary.
+# The fetch is HEAD-scoped (reads only this commit's own cache scope). The warm is fail-safe
+# (any failure → just the remote fetch) and its source is hardcoded, so nothing can redirect
+# the download off the trusted master pipeline.
+name: Get cache
+description: Get this commit's oleans into the local cache.
+inputs:
+  working_directory:
+    description: The lake project to fetch the cache for (e.g. the checked-out PR branch).
+    required: true
+  cache_bin:
+    description: Path to the trusted `cache` binary, relative to `working_directory`.
+    required: true
+runs:
+  using: composite
+  steps:
+    # 1. Warm cache from the GitHub artifact. Resolve which snapshot to use: the one built
+    #    at this commit's merge-base with master (its unchanged files hash identically
+    #    there), else the newest still-retained one at-or-before it, else the latest (a
+    #    merge-base older than retention, or any failure, lands here). Canonical repo only.
+    - name: Resolve cache snapshot
+      id: resolve
+      if: ${{ github.repository == 'leanprover-community/mathlib4' }}
+      shell: bash
+      env:
+        GH_TOKEN: ${{ github.token }}
+        HEAD_SHA: ${{ github.event.pull_request.head.sha || github.sha }}
+      run: |
+        set -uo pipefail
+        runs="repos/leanprover-community/mathlib4/actions/workflows/build.yml/runs?branch=master&event=push&status=success"
+
+        # Each helper prints a matching successful master-push run-id, or empty.
+        run_at()     { gh api "${runs}&head_sha=$1" --jq '.workflow_runs[0].id // empty' 2>/dev/null || true; }
+        latest_run() { gh api "${runs}&per_page=1"  --jq '.workflow_runs[0].id // empty' 2>/dev/null || true; }
+        # newest run created at-or-before date $1, but not older than cutoff $2
+        newest_before() {
+          gh api "${runs}&per_page=100" 2>/dev/null | jq -r --arg d "$1" --arg c "$2" \
+            '[.workflow_runs[] | select(.created_at <= $d and ($c == "" or .created_at >= $c))][0].id // empty' \
+            2>/dev/null || true
+        }
+        # True if run-id $1 actually carries a `cache-snapshot` artifact. Older runs
+        # predate the feature and artifacts expire, so a successful run is not enough.
+        # Filters server-side by name, but re-checks in jq in case `name` is ignored.
+        has_snapshot() {
+          [[ -n "$(gh api "repos/leanprover-community/mathlib4/actions/runs/$1/artifacts?name=cache-snapshot&per_page=100" \
+            --jq '.artifacts[] | select(.name == "cache-snapshot") | .id' 2>/dev/null | head -1 || true)" ]]
+        }
+
+        # This PR's merge-base with master (+ its commit date), and the cutoff below which
+        # snapshots have expired (retention ~14d).
+        mb_info=$(gh api "repos/leanprover-community/mathlib4/compare/master...${HEAD_SHA}" \
+          --jq '.merge_base_commit | "\(.sha) \(.commit.committer.date)"' 2>/dev/null || true)
+        read -r mb mb_date <<< "${mb_info}"
+        cutoff=$(date -u -d '13 days ago' +%Y-%m-%dT%H:%M:%SZ 2>/dev/null || true)
+
+        # Prefer the merge-base's snapshot (while still retained), then the newest one
+        # before it, then the latest of all.
+        run_id=""
+        if [[ -n "${mb}" && ( -z "${cutoff}" || "${mb_date}" > "${cutoff}" ) ]]; then
+          run_id=$(run_at "${mb}")
+          [[ -z "${run_id}" ]] && run_id=$(newest_before "${mb_date}" "${cutoff}")
+        fi
+        [[ -z "${run_id}" ]] && run_id=$(latest_run)
+
+        # The resolved run may carry no `cache-snapshot` artifact: an older merge-base
+        # predating the feature, or one whose artifact already expired (older-than-today
+        # runs often won't have one). Rather than let the download step hard-error on a
+        # missing artifact, confirm it's present; if not, fall back to the latest master
+        # run, and warm only if that one has it.
+        if [[ -n "${run_id}" ]] && ! has_snapshot "${run_id}"; then
+          echo "Run ${run_id} has no cache-snapshot artifact; falling back to latest master run."
+          run_id=$(latest_run)
+          if [[ -n "${run_id}" ]] && ! has_snapshot "${run_id}"; then
+            run_id=""
+          fi
+        fi
+
+        echo "Resolved cache-snapshot run_id: '${run_id}' (merge-base: ${mb:-unknown})"
+        echo "run_id=${run_id}" >> "$GITHUB_OUTPUT"
+
+    - name: Warm cache from GitHub artifact
+      if: ${{ steps.resolve.outputs.run_id != '' }}
+      continue-on-error: true # fail-safe: fall back to the remote fetch (step 2)
+      uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
+      with:
+        name: cache-snapshot
+        path: /home/lean/.cache/mathlib
+        repository: leanprover-community/mathlib4
+        run-id: ${{ steps.resolve.outputs.run_id }}
+        github-token: ${{ github.token }}
+
+    # 2. Fetch this commit's oleans from the remote cache with the trusted `cache` binary
+    #    (outside landrun). Runs on every repo; the warm above just gives the canonical
+    #    repo a local head start. HEAD-scoped: reads only this commit's own cache scope.
+    - name: Fetch cache from remote
+      shell: bash
+      env:
+        WORKDIR: ${{ inputs.working_directory }}
+        CACHE_BIN: ${{ inputs.cache_bin }}
+        CACHE_REPO: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
+      run: |
+        set -eo pipefail
+        cd "${WORKDIR}"
+        rm -rf .lake/build/lib/lean/Mathlib
+        log="${RUNNER_TEMP:-/tmp}/cache-get.log"
+        # --repo so fork PRs also read their own repo-namespaced cache (master is read flat,
+        # so this still gets the master bulk); for in-repo runs it resolves to the same repo.
+        "${CACHE_BIN}" --repo="${CACHE_REPO}" get 2>&1 | tee "${log}"
+        # Warmth = how much the snapshot covered HEAD: files already cached locally
+        # (just decompressed) vs downloaded from Azure. Parsed best-effort from the log.
+        warm=$(grep -oE 'Decompressing [0-9]+ already-cached' "${log}" | grep -oE '[0-9]+' | head -1 || true)
+        cold=$(grep -oE 'Attempting to download [0-9]+' "${log}" | grep -oE '[0-9]+' | head -1 || true)
+        echo "Cache warmth: ${warm:-0} already-cached (warm) / ${cold:-0} downloaded from Azure (cold)"

.github/actions/get-mathlib-ci/README.md

@@ -25,7 +25,7 @@ then use the local action:
 
 ```yaml
 - name: Checkout local actions
-  uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+  uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
   with:
     ref: ${{ github.workflow_sha }}
     fetch-depth: 1

.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: 5aee9d4ce5a39050c72b4aa46015a824b0c189ac
+    default: 5668fbbccf0fecefdfcddf539b8406db197dfc59
   path:
     description: Checkout destination path.
     required: false
@@ -33,7 +33,7 @@ runs:
   using: composite
   steps:
     - name: Get mathlib-ci
-      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       with:
         repository: leanprover-community/mathlib-ci
         ref: ${{ inputs.ref }}

.github/actions/get-tools/action.yml

@@ -139,7 +139,7 @@ runs:
 
     - name: Checkout tools branch (source build)
       if: ${{ steps.finalize.outputs.result == 'build' }}
-      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       with:
         ref: ${{ inputs.tools_source_ref }}
         path: ${{ inputs.path }}