ci(cache): consolidate cache fetching into one action, warmed from master (leanprover-community#40678)

marcelolynch · ReemMelamed · commit e621348b24c1 · 2026-06-20T15:20:05.000+03:00
Consolidates the build job's cache fetch into a single `get-cache` action. It used to be a 3-step sequence (a cold-cache probe, a landrun verify, then a parent-commit warmup plus the fetch); now one action runs a single HEAD-scoped `cache get`, optionally warmed from a free master snapshot. Two things come out of that: - HEAD-scoped fetch: dropping the parent-commit warmup (which checked out other SHAs and read their cache) means a run reads only its own scope plus the trusted master snapshot, matching the per-commit scope from leanprover-community#40035. - Warmed from master: master's `.ltar` set is otherwise re-read from the paid Azure cache on every cold runner. The master `push` build in `build.yml` now publishes it once as a free `cache-snapshot` artifact, pruned to that commit's set and reusing what is already on disk, so it adds no Azure read. The action seeds `~/.cache/mathlib` from the snapshot at the PR's merge-base (its unchanged files hash identically there), else the newest one at-or-before it, else the latest, before fetching, so the unchanged-from-master oleans come from GitHub rather than Azure. The snapshot download is trust-pinned to master push runs and fail-safe (any problem falls back to a plain Azure `cache get`), and fork-safe because `pull_request_target` runs the base branch's workflow and actions rather than the PR's. Each run logs a warm/cold count. `bors.yml` and `ci_dev.yml` gain read-only `actions: read`. Snapshot retention is 14 days, and `.ltar` are input-hash-keyed, so a stale base falls back gracefully.
diff --git a/.github/actions/get-cache/action.yml b/.github/actions/get-cache/action.yml
@@ -0,0 +1,95 @@
+# 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
+        }
+
+        # 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)
+
+        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)"
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -16,6 +16,7 @@ concurrency:
 permissions:
   contents: read
   id-token: write
+  actions: read  # download master artifacts (tools-bin, cache-snapshot)
   pull-requests: write  # Only allow PR comments/labels
   # All other permissions are implicitly 'none'
 
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -70,5 +70,7 @@ jobs:
                && 'cache-upload-forks'
           || ''
         }}
+      # the single producer: the master `push` build
+      publish_cache: ${{ github.repository == 'leanprover-community/mathlib4' && github.event_name == 'push' && github.ref == 'refs/heads/master' }}
       runs_on: pr
     secrets: inherit
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -9,10 +9,9 @@ on:
       - 'staging*.tmp'
       - 'nolints'
     paths-ignore:
-      # pull_request_target uses the workflow from the target branch:
-      # PR changes under this directory won't affect this run, so
-      # running it is just wasteful
-      - '.github/workflows/**'
+      # pull_request_target runs the workflow and its actions from the target branch, not
+      # the PR, so PR changes under these dirs can't affect the run — triggering is wasteful.
+      - '.github/**'
 
 concurrency:
   # label each workflow run; only the latest with each label will run
diff --git a/.github/workflows/build_template.yml b/.github/workflows/build_template.yml
@@ -33,6 +33,12 @@ on:
         # federated credential is scoped to; it must match the writer `cache_application_id`.
         type: string
         required: true
+      publish_cache:
+        # On a successful build, publish this run's `.ltar` set as `cache-snapshot`.
+        # Set by callers ONLY for the master-`push` build — the single producer.
+        type: boolean
+        required: false
+        default: false
 
 env:
   # Disable Lake's automatic fetching of cloud builds.
@@ -51,7 +57,6 @@ jobs:
       archive-outcome: ${{ steps.archive.outcome }}
       counterexamples-outcome: ${{ steps.counterexamples.outcome }}
       cache-staging-has-files: ${{ steps.cache_staging_check.outputs.has_files }}
-      get-cache-outcome: ${{ steps.get.outcome }}
       lint-outcome: ${{ steps.lint.outcome }}
       mk_all-outcome: ${{ steps.mk_all.outcome }}
       noisy-outcome: ${{ steps.noisy.outcome }}
@@ -313,95 +318,12 @@ jobs:
             echo "✅ All inputRevs in lake-manifest.json are valid"
           fi
 
-      - name: get cache (1/3 - setup and initial fetch)
-        id: get_cache_part1_setup
-        shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
-        run: |
-          cd pr-branch
-          echo "Removing old Mathlib build directories prior to cache fetch..."
-          rm -rf .lake/build/lib/lean/Mathlib
-
-          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
-          ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
-
-      - name: get cache (2/3 - test Mathlib.Init cache)
-        id: get_cache_part2_test
-        continue-on-error: true # Allow workflow to proceed to Part 3 to check outcome
-        # This step uses the job's default shell, which is landrun-wrapped bash
-        run: |
-          cd pr-branch
-
-          echo "Attempting: lake build --no-build -v Mathlib.Init (this runs under landrun)"
-          lake build --no-build -v Mathlib.Init
-
-      - name: get cache (3/3 - finalize cache operation)
-        id: get
-        shell: bash # only runs git and `cache get` from `tools-branch`, so doesn't need to be inside landrun
-        env:
-          BEFORE_SHA: ${{ github.event.before || '' }}
-          BASE_SHA: ${{ github.event.pull_request.base.sha || '' }}
-          CACHE_REPO: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
-        run: |
-          cd pr-branch
-          if [[ "${{ steps.get_cache_part2_test.outcome }}" != "success" ]]; then
-            echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
-            echo "No cache for 'Mathlib.Init' available or it could not be prepared."
-            exit 0
-          fi
-
-          ORIG_SHA="$(git rev-parse HEAD)"
-          PREV_SHA=""
-          PREV_SHA_SOURCE=""
-
-          # When a ref is newly created, github.event.before can be all-zero.
-          if [[ "$BEFORE_SHA" =~ ^0{40}$ ]]; then
-            BEFORE_SHA=""
-          fi
-
-          if [[ -n "$BEFORE_SHA" ]]; then
-            PREV_SHA="$BEFORE_SHA"
-            PREV_SHA_SOURCE="github.event.before"
-          elif [[ -n "$BASE_SHA" ]]; then
-            PREV_SHA="$BASE_SHA"
-            PREV_SHA_SOURCE="pull_request.base.sha"
-          else
-            PREV_SHA="$(git rev-parse --verify --quiet HEAD^ || true)"
-            if [[ -n "$PREV_SHA" ]]; then
-              PREV_SHA_SOURCE="HEAD^"
-            fi
-          fi
-
-          if [[ -n "$PREV_SHA" ]]; then
-            # cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
-            echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
-            if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
-              # Skip warmup if the previous commit uses a different toolchain
-              PREV_TOOLCHAIN=$(git show "$PREV_SHA:lean-toolchain" 2>/dev/null || true)
-              if [[ "$PREV_TOOLCHAIN" != "$(cat lean-toolchain)" ]]; then
-                echo "Previous commit $PREV_SHA uses a different toolchain ($PREV_TOOLCHAIN); skipping warmup."
-              else
-                git checkout "$PREV_SHA"
-                ../tools-branch/.lake/build/bin/cache get
-                # Run again with --repo, to ensure we actually get the oleans.
-                ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
-
-                echo "Switching back to branch head"
-                git checkout "$ORIG_SHA"
-              fi
-            else
-              echo "Could not fetch $PREV_SHA; skipping parent warmup cache fetch."
-            fi
-          else
-            echo "No previous commit candidate found; skipping parent warmup cache fetch."
-          fi
-
-          echo "Fetching all remaining cache..."
-
-          ../tools-branch/.lake/build/bin/cache get
-
-          # Run again with --repo, to ensure we actually get the oleans.
-          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
+      # Get this commit's oleans into the local cache — see the action for the steps.
+      - name: Get cache
+        uses: ./workflow-actions/.github/actions/get-cache
+        with:
+          working_directory: pr-branch
+          cache_bin: ../tools-branch/.lake/build/bin/cache
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -522,6 +444,30 @@ jobs:
           name: cache-staging
           path: cache-staging/
 
+      # Prune to this commit's `.ltar` set so the published snapshot is exactly master's
+      # current cache (the local dir also holds the previous snapshot it warmed from).
+      - name: prune local cache to this commit's set
+        if: ${{ inputs.publish_cache && steps.build.outcome == 'success' }}
+        continue-on-error: true # best-effort; never fail the build
+        shell: bash # runs the trusted tools-branch `cache` binary, so no landrun needed
+        run: |
+          cd pr-branch
+          ../tools-branch/.lake/build/bin/cache clean
+
+      # Publish this run's pruned `.ltar` set as `cache-snapshot` for other runs to warm
+      # from. Already on disk (no Azure egress) and already zstd-compressed (skip
+      # recompression); retention covers how far back a PR's merge-base can be matched.
+      - name: upload cache snapshot warming artifact
+        if: ${{ inputs.publish_cache && steps.build.outcome == 'success' }}
+        continue-on-error: true # best-effort; never fail the build
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        with:
+          name: cache-snapshot
+          path: /home/lean/.cache/mathlib/*.ltar
+          compression-level: 0
+          retention-days: 14
+          if-no-files-found: warn
+
       - name: Check if building Archive or Counterexamples failed
         if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
         run: |
diff --git a/.github/workflows/ci_dev.yml b/.github/workflows/ci_dev.yml
@@ -28,6 +28,7 @@ on:
 permissions:
   contents: read
   id-token: write
+  actions: read  # read-only: download master artifacts (tools-bin, cache-snapshot)
   # By default let's remove this permission (which is present in the other build pipelines)
   # from the CI experimentation runs to avoid unwitting side effects
   # pull-requests: write
