ci: warm master's build from the staging cache artifact

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

@@ -1,5 +1,7 @@
 # Get this commit's oleans, in two phases:
-#   1. Warm the cache from the `cache-snapshot` GitHub artifact (canonical repo only).
+#   1. Warm the cache from the `cache-snapshot` GitHub artifact (canonical repo only). With
+#      `warm_from_staging`, also warm it from the `cache-staging` artifact of this commit's
+#      staging run.
 #   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
@@ -13,6 +15,12 @@ inputs:
   cache_bin:
     description: Path to the trusted `cache` binary, relative to `working_directory`.
     required: true
+  warm_from_staging:
+    description: >
+      'true' to also warm the cache from the `cache-staging` artifact of the bors staging run
+      at this commit. Only master pushes set it: bors fast-forwards master to a staging commit.
+    required: false
+    default: 'false'
 runs:
   using: composite
   steps:
@@ -98,6 +106,74 @@ runs:
         run-id: ${{ steps.resolve.outputs.run_id }}
         github-token: ${{ github.token }}
 
+    # The staging run at this commit built the files that the master container did not hold
+    # before this commit. Staging is the trusted lane that uploaded them to the master
+    # container, so its artifact holds the same trusted files.
+    - name: Resolve staging cache artifact
+      id: resolve_staging
+      if: ${{ inputs.warm_from_staging == 'true' && github.repository == 'leanprover-community/mathlib4' }}
+      shell: bash
+      env:
+        GH_TOKEN: ${{ github.token }}
+      run: |
+        set -uo pipefail
+        api() { local out; out=$(gh api "$@" 2>/dev/null) && printf '%s\n' "${out}"; }
+        cutoff=$(date -u -d '2 days ago' +%Y-%m-%dT%H:%M:%SZ)
+        # bors fast-forwards master once the required jobs pass, so the staging run can still
+        # be in progress: select runs by commit, not by conclusion. Only a run that bors
+        # started, and that nobody else re-ran, qualifies.
+        run_ids=$(api "repos/leanprover-community/mathlib4/actions/workflows/bors.yml/runs?branch=staging&event=push&head_sha=${GITHUB_SHA}&created=>=${cutoff}&per_page=10" \
+          --jq '.workflow_runs[] | select(.actor.login == "mathlib-bors[bot]" and .triggering_actor.login == "mathlib-bors[bot]") | .id')
+        run_id=""
+        for id in ${run_ids}; do
+          if api "repos/leanprover-community/mathlib4/actions/runs/${id}/artifacts?name=cache-staging&per_page=100" \
+              --jq '[.artifacts[] | select(.name == "cache-staging" and .expires_at > (now | todate))][0] // empty' \
+              | grep -q .; then
+            run_id="${id}"
+            break
+          fi
+        done
+        echo "Resolved staging cache-staging run_id: '${run_id}'"
+        echo "run_id=${run_id}" >> "$GITHUB_OUTPUT"
+
+    # The download goes to a temporary directory, so a failed or partial download leaves no
+    # `.ltar` file in the local cache, where `cache get` would treat it as already cached.
+    - name: Download the staging artifact
+      id: download_staging
+      if: ${{ steps.resolve_staging.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-staging
+        path: ${{ runner.temp }}/staging-ltar
+        repository: leanprover-community/mathlib4
+        run-id: ${{ steps.resolve_staging.outputs.run_id }}
+        github-token: ${{ github.token }}
+
+    # A `.ltar` name is the hash of the module's inputs, so a file already in the local cache
+    # stays and the artifact's file of the same name is dropped.
+    - name: Warm cache from the staging artifact
+      if: ${{ steps.download_staging.outcome == 'success' }}
+      continue-on-error: true # fail-safe: fall back to the remote fetch (step 2)
+      shell: bash
+      run: |
+        set -euo pipefail
+        shopt -s nullglob
+        dir="${RUNNER_TEMP}/staging-ltar"
+        cache=/home/lean/.cache/mathlib
+        moved=0
+        skipped=0
+        for f in "${dir}"/*.ltar; do
+          if [ -e "${cache}/${f##*/}" ]; then
+            skipped=$((skipped + 1))
+          else
+            mv "${f}" "${cache}/"
+            moved=$((moved + 1))
+          fi
+        done
+        rm -rf "${dir}"
+        echo "Moved ${moved} .ltar file(s) from the staging artifact into the local cache; skipped ${skipped} that the local cache already held."
+
     # 2. Fetch this commit's oleans from the remote cache with the trusted `cache` binary.
     #    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.

.github/workflows/build_template.yml

@@ -177,6 +177,7 @@ jobs:
         with:
           working_directory: pr-branch
           cache_bin: ../tools-branch/.lake/build/bin/cache
+          warm_from_staging: ${{ inputs.publish_cache }}
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -507,6 +508,7 @@ jobs:
         with:
           working_directory: pr-branch
           cache_bin: ../tools-branch/.lake/build/bin/cache
+          warm_from_staging: ${{ inputs.publish_cache }}
 
       - name: verify the Mathlib cache is complete
         # Enforced only when the build succeeded (then the cache must be complete):