Skip to content

Commit 1b0782d

Browse files
committed
chore(cache): Stop dual-writing the cache to the legacy container (leanprover-community#40907)
With this PR, master CI now uploads only to the `master` container, and the `legacy` (bare `mathlib4`) container stays as a read-only endpoint for pre-refactor artifacts.
1 parent f07d120 commit 1b0782d

2 files changed

Lines changed: 7 additions & 19 deletions

File tree

.github/workflows/build_template.yml

Lines changed: 2 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -694,21 +694,8 @@ jobs:
694694
# $MATHLIB_CACHE_PRIMARY is set by the `Compute cache trust dispatch`
695695
# step above, from the shared composite action that owns the (repo,
696696
# branch) → container mapping for both this job and the read-side
697-
# jobs (build, post_steps).
698-
# Dual-write to the legacy `mathlib4` container first, then the
699-
# primary. Only master CI dual-writes: older cache tools read only
700-
# `legacy`, so it must stay fresh for them, while forks and nightly
701-
# never write `legacy` (keeping low-trust artifacts out of what those
702-
# readers trust). Writing `legacy` first keeps it a superset of
703-
# `master` for as long as we dual-write: with `set -e`, a failed
704-
# legacy write aborts the step before `master` gets artifacts that
705-
# `legacy` lacks. (`put-staged` exits non-zero on real upload
706-
# failures; already-present 409/412 blobs are not failures.)
707-
if [ "$MATHLIB_CACHE_PRIMARY" = "master" ]; then
708-
echo "Dual-writing to legacy container first (keeps legacy a superset of master)..."
709-
lake env "$CACHE_BIN" put-staged --container=legacy --staging-dir="cache-staging" --repo="$REPO"
710-
fi
711-
697+
# jobs (build, post_steps). Each job writes only into its own trust-level
698+
# container.
712699
echo "Uploading cache to Azure (container: $MATHLIB_CACHE_PRIMARY)..."
713700
lake env "$CACHE_BIN" put-staged --container="$MATHLIB_CACHE_PRIMARY" --staging-dir="cache-staging" --repo="$REPO"
714701

Cache/Infra.lean

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,10 +51,11 @@ inductive Container where
5151
| nightlyTesting
5252
/-- Container for toolchain-PR test runs. -/
5353
| prToolchainTests
54-
/-- The bare `mathlib4` container that older cache clients read from. Only
55-
master CI writes here (mirroring its `mathlib4-master` upload), so those
56-
clients keep finding master-built artifacts; forks and nightly-testing stay
57-
out to keep low-trust writes from reaching readers that predate the split. -/
54+
/-- The bare `mathlib4` container that older cache clients read from. CI does
55+
not upload here; it is a read-only store of the master-built artifacts that
56+
were mirrored from `mathlib4-master`, kept reachable so those older clients
57+
can resolve them. The `master` container is a self-contained cache, so reads
58+
fall back to `legacy` only for artifacts predating the write cutover. -/
5859
| legacy
5960
deriving DecidableEq, Repr, BEq, Inhabited
6061

0 commit comments

Comments
 (0)