[marcelolynch]

The master build warms its local cache from the cache-snapshot artifact of the previous master commit. After a large bors batch, this snapshot does not hold the new files of the batch, so the Build and Test-and-lint jobs download thousands of files from the remote cache. In the 14 days to 2026-10-21, three of the five failed master runs failed on one broken transfer in such a download (3,860 to 8,629 files).

This PR adds a second warm step to the get-cache action. When the new input warm_from_staging is true, the action finds the bors staging run at the same commit and downloads its cache-staging artifact into a temporary directory. After a complete download, it moves the .ltar files that the local cache lacks into it, so a failed download leaves no partial file there and no existing file is replaced. The staging run is the trusted run that uploaded these files to the master container. build_template.yml sets the input from publish_cache, so only master pushes use it. When no staging run or artifact exists, the action continues with the remote fetch.

The step selects the staging run by commit, not by conclusion: bors fast-forwards master when the required jobs pass, before the whole staging run completes. It accepts only a run that mathlib-bors[bot] started and that nobody re-ran. The step logs how many files it moved and how many the local cache already held.

The artifact holds only the files that the staging run built, so the master build still fetches the files that the staging run downloaded.

#45096 retries the broken transfers. This PR removes most of the transfers on master.

A fork PR runs master's workflows, so the CI of this PR does not run the changed workflow.

The resolve step finds run 39614558840 for commit a2f40e9 and no artifact for a documentation-only commit; actionlint and shellcheck pass.

🤖

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to Zulip and join the Lean community.
Thank you again for joining our community.

[github-actions]

PR summary 028732138e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 028732138e
Reference commit 4530ed722e

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

• .github/workflows/build_template.yml