chore(ci): cache dependencies in the lake cache shadow pipeline

[marcelolynch]

This PR makes the lake cache shadow pipeline cache dependencies. The pipeline previously cached the root package only, and used the legacy cache for the dependencies.

The sections below explain the mechanism. They also go in .github/workflows/lake_cache_shadow.md, which this PR adds. The workflow header used to carry the design; it now points at that document, and the comments in the workflow cover what each step does.

The pipeline caches every git dependency in mathlib's manifest, 8 of them today. For each dependency, <DEP> is its name, <R-DEP> is its revision from the manifest, and <S-DEP> is its scope, mathlib4-master-shadow/deps/<toolchain-slug>/<pin-hash>/<DEP>. The pin hash is a short fingerprint of the revisions that mathlib's manifest pins, and the toolchain slug is the toolchain with its punctuation replaced; both are explained below. A rendered scope reads mathlib4-master-shadow/deps/leanprover-lean4-v4.34.0-rc2/2d10dd67/batteries.

Cache service configuration

Every lake cache call passes --service=shadow. Each job writes that service definition itself, into the file LAKE_CONFIG names, because each job runs on its own runner:

[[cache.service]]
name = "shadow"
type = "s3"
artifactEndpoint = "https://pub-<hash>.r2.dev/<prefix>/artifacts"
revisionEndpoint = "https://pub-<hash>.r2.dev/<prefix>/revisions"

A job that fetches writes the public read endpoints, as above. The upload job writes the authenticated S3 endpoints, and LAKE_CACHE_KEY signs its requests. A services file is the supported way to configure a cache service, and Lake deprecates the endpoint environment variables.

Push, from a clean cache

Lake's -o records the mappings of the workspace root only, so step 3 loads each dependency as its own root. Step 1 runs once, and steps 2 to 5 run once per dependency.

1. lake build Mathlib builds mathlib and every dependency from source, and writes the artifacts into the local Lake cache.

2. Write <DEP>-overrides.json. A jq filter reads mathlib's lake-manifest.json, drops the entry for <DEP> itself, and rewrites each remaining package as a path entry into this checkout. It keeps the name, scope, configFile and inherited fields, sets type to path, and sets dir to .lake/packages/<name>. For aesop it renders:

    {"version": "1.2.0",
     "packages": [
       {"name": "batteries", "scope": "leanprover-community",
        "configFile": "lakefile.toml", "inherited": false, "type": "path",
        "dir": "<checkout>/.lake/packages/batteries"},
       ... one entry per other package ...
     ]}
   

   The file pins the dependencies of <DEP> to mathlib's. Without it Lake uses the manifest of <DEP>, and the mappings never match this workspace's input hashes.

3. Export: lake -d .lake/packages/<DEP> build --packages=.lake/dep-plan/<DEP>-overrides.json -o .lake/dep-outputs/<DEP>.jsonl. This load replays instead of compiling, because step 1 filled the local cache.

4. Stage: lake cache stage .lake/dep-outputs/<DEP>.jsonl lake-cache-staging/deps/<DEP>. Each dependency needs its own directory, because cache stage writes one outputs.jsonl per directory. The staging tree travels to the upload job as a GitHub artifact, because the build runs in a sandbox without the credentials.

5. Upload: lake cache put-staged lake-cache-staging/deps/<DEP> --service=shadow --scope=<S-DEP> --rev=<R-DEP>. Lake PUTs the artifacts first and the revision file last.

All five steps, the two scope qualifiers described below, and the lakefile patch that enables Lake's artifact cache are required for a full hit on the root package and its dependencies. Without any one of them a fetch returns mappings that do not match, and the modules rebuild.

Pull

The consume job builds mathlib from the bucket alone. It sets LAKE_NO_CACHE, so the bucket accounts for every replay.

1. lake cache get --service=shadow --scope=mathlib4-master-shadow --rev=<mathlib-sha>.
2. lake cache get --service=shadow --package=<DEP> --scope=<S-DEP> --rev=<R-DEP>, once per dependency, with the revisions from mathlib's manifest.
3. lake build Mathlib replays both.

The downstream job runs the same pull for a small project that requires mathlib. In that project mathlib is a dependency, so it comes from the root scope under its sha.

What a warm run adds

Four optimizations decide how much a run compiles and uploads. None of them changes the keys or the content that a run writes.

• The probe. Before the build, curl -fsS -o /dev/null "$REVISION_ENDPOINT/<S-DEP>/<R-DEP>.jsonl" asks whether the bucket already holds this dependency. If it does, steps 2 to 5 skip it. A revision, a toolchain and a pin set determine the content, so a dependency uploads once. Later runs skip it, until a manifest bump or a toolchain bump changes the scope.
• The root warm start. lake cache get --service=shadow --scope=mathlib4-master-shadow --rev=<previous-sha> seeds the local cache from the previous run on this toolchain, so step 1 compiles the churn since that run only. analysis/<toolchain-slug>/_latest.txt holds the previous sha.
• The dependency warm start. lake cache get --service=shadow --package=<DEP> --scope=<S-DEP> --rev=<R-DEP> for each dependency the probe found, so step 1 replays it instead of compiling it.
• The legacy cache, for a cold analysis chain only, where no previous run exists to warm start from.

The --rev arguments are an optimization too. Without them Lake searches back through the ancestors of the checkout's HEAD.

Dependency scopes

Lake requires --scope or --repo on every put and get against a custom endpoint; there is no unscoped form. A scope also bounds where a content hash is trusted, because Lake does not use cryptographically secure hashes and prefixes uploads to avoid clashes. Each package therefore gets its own namespace for its artifacts and its revision files, and the root scope stays for mathlib alone. --repo=<owner>/<package> would give a scope of that shape, and Lake would add the toolchain and the platform to it. It has no place for the pin hash, so the pipeline passes the whole string to --scope, which Lake uses verbatim.

Two qualifiers extend a dependency scope. The toolchain slug separates the toolchains that build one long-lived revision. The pin hash separates the manifest generations: the input hashes of a dependency cover the artifacts of its upstreams, so a bump of batteries alone changes the correct mappings for aesop but not the revision of aesop.

A dependency's entry is revisions/<S-DEP>/<R-DEP>.jsonl, so four things identify it: the dependency, its revision, the toolchain, and the pin set. A mathlib commit changes none of them, which is why the steady state uploads no dependency. A toolchain bump changes the slug, and a dependency bump changes both that dependency's revision and the pin hash. The pin hash covers the whole manifest, so one dependency bump currently re-keys all of them; a hash over each dependency's own upstream closure would re-key only the affected ones. Every job runs on Linux, so the scope carries no platform segment.

Storage layout

One bucket holds these keys:

revisions/mathlib4-master-shadow/<mathlib-sha>.jsonl
artifacts/mathlib4-master-shadow/<content-hash>.art
revisions/<S-DEP>/<R-DEP>.jsonl
artifacts/<S-DEP>/<content-hash>.art
analysis/leanprover-lean4-v4.34.0-rc2/_latest.txt
analysis/leanprover-lean4-v4.34.0-rc2/<mathlib-sha>.txt

lake cache get --scope=<SCOPE> --rev=<REV> reads revisions/<SCOPE>/<REV>.jsonl, which maps input hashes to artifacts, and downloads the artifacts/<SCOPE>/<content-hash>.art files it names. Lake does not know the analysis/ prefix; the workflow owns it. _latest.txt holds the sha the next run warm starts from, and <mathlib-sha>.txt holds its carryover baseline.

Other changes

Other changes:

• The legacy cache becomes a bootstrap fallback for a cold analysis chain, so a pinned run hydrates from the shadow scope and compiles the churn since the previous run.
• proofwidgets is cached like every other dependency. It commits its npm output and the traces that guard the npm steps.
• The new downstream job sets MATHLIB_NO_CACHE_ON_UPDATE=1, because mathlib's post-update hook otherwise hides what the bucket serves.
• The scope qualifiers are derived once, in the plan step, and published as job outputs. The downstream job derives its own, because a real downstream project has no access to mathlib's CI outputs.

Validation

Ten dispatch runs cover the clean push, the steady state, the override lane and the downstream project: run 4, run 5, run 7. They report zero root-package rebuilds, 8 of 8 dependencies fetched with zero rebuilds, and 9 of 9 packages fetched downstream with zero Mathlib rebuilds. A run fails if a root-package module rebuilds, so the daily run guards against a regression. A steady-state run takes about 11 minutes.

The pipeline needs lake cache get --package, which the repo pin v4.34.0-rc2 provides. An older toolchain override builds from source and warns.
🤖 Generated with Claude Code

[github-actions]

PR summary 02c421ac6f

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 02c421ac6f
Reference commit 23a3216f0e

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/lake_cache_shadow.md
• .github/workflows/lake_cache_shadow.yml