Commit 2026-06-15 19:17 05bdd16f

View on Github →

feat(cache): restructure cache tool server-side storage layout (#40035) This PR significantly restructures the cache back-end storage layout to address some security issues and as a side benefit improve auditing, garbage collection, provenance.

Instead of setting the cache-universe boundary to the repository, we scope it to particular commit SHAs. This means a review of the changes in a PR does give you confidence in pulling from the cache at that commit.
Split the cache universes from master, forks, and nightly-testing at the infrastructure level, using different azure containers. This has other benefits in management, like better auditing, the possibility of targeted garbage collection, etc. See SECURITY.md for the motivation and explanation of the trust model implemented here. Also added cache tool tests, and changed a bunch of the messages output to users to surface security concerns more clearly. Extra details:

Trust model

Five containers — master, forks, nightly-testing, pr-toolchain-tests, and legacy (the original bare mathlib4 bucket) — each mapped to a dedicated Azure container. Every trust level has its own writer identity. Azure RBAC on the OIDC token is the enforced write boundary, not the workflow logic.
Reads use a per-repo, trust-ordered chain (most-trusted first, stop at first hit
URL layout is fixed per container, not per repo: master is flat (/f/{hash}), multi-writer containers namespace by repo (/f/{repo}/{hash}), legacy preserves its historical mixed layout for older clients.

Per-commit scoping & discovery

Fork uploads are scoped to their commit SHA (/f/{repo}/{sha}/{hash}), so a closed/hidden PR's artifacts can't be served to a later honest PR on the same fork. A marker blob (/m/{repo}/{sha}) is written after a successful upload.
New cache query [REF]: walks history to the merge-base with master and HEAD- probes markers to report the most recent cached commit (or a boolean probe for a single ref). cache get --scope=<sha> then reads that commit's namespace.
cache get --unsafe folds that discovery into the download itself: it walks history for the most recent cached fork commit and reads it as a scope automatically, instead of you copying a SHA into --scope. --unsafe-window=N widens this to the N most recent (default 1). It always prints the security notice, since it trusts whoever built those commits.
cache get prints a security notice whenever a read leaves the repo's default trust boundary (a scope, a widened --cache-from, or a --repo that diverges from the git remote), plus a hint pointing uncached fork HEADs at cache query.

CLI / env surface

New flags: --cache-from=LIST, --container=NAME, --scope=REF, --unsafe, --unsafe-window=N; new command cache query.
New env: MATHLIB_CACHE_FROM, MATHLIB_CACHE_REPO_SCOPE. MATHLIB_CACHE_GET_URL / _PUT_URL retained as single-URL escape hatches; MATHLIB_CACHE_USE_CLOUDFLARE removed.

CI wiring

New composite action cache-trust-dispatch is the single source mapping (repo, branch) → (write container, read chain, per-commit scope); build.yml, bors.yml, and build_template.yml consult it. Trust policy lives in YAML, not in the Lean tool.
During migration, master CI dual-writes to legacy so older cache clients keep working; forks/nightly never write to legacy.

Code organization & testing

Backend split into focused modules: Cache.Infra (container model), Cache.Cli (option parsing), Cache.Marker, Cache.Query, Cache.Warning; Cache.Init folded away.
New standalone lake exe cache-test (Cache.Test) unit-tests the pure logic — container model, URL construction, per-repo read chains, flag parsing, and the warning conditions — without building Mathlib.