[Heidi Howard (heidihoward)]

Motivation

This is an alternative to #8702 that retains Mathlib and the current mathematical definitions, theorem statements, proof implementations, dependency revisions, and lint drivers.
It targets dependency provisioning and storage rather than replacing the sequence and finite-set types used in the specifications.

Changes

• Put remote dependencies for all five Lean packages under lean/.lake/packages, retaining separate first-party build outputs.
• Add scripts/lean-setup.sh to fetch only the cache closure required by each package's direct Mathlib imports and shared common imports, plus Batteries' lint-driver dependencies where needed.
• Include private imports and import all, deduplicate module names, and exclude generated .lake trees from discovery.
• Create package-local .lake/packages compatibility symlinks before fetching caches.
• Replace the four unrestricted cache-fetch call sites in the package/replay workflows and update documented setup commands.
• Cache the new shared dependency location, bump the cache namespace to v3, and invalidate by toolchain, platform/architecture, dependency configuration, setup implementation, and required module list.
• Hash the module list separately: proof-only edits can retain dependency cache hits, while changing the required module set creates a new cache entry.
• Run setup regression tests in the common package job and trigger Lean CI when the helper or its tests change.

No .lean source file or locked dependency revision changes.
Kernel/axiom checks, import coverage, architecture checks, linters, replay fixtures, and the complete library roots are retained.

Local measurements

These are local sequential-package measurements, not measurements of GitHub Actions performance.
The benchmark used three fresh source snapshots at 956411001165b447107261089b9bc54584e4985a, Lean v4.35.0, Linux x86_64 with 8 logical processors and approximately 15 GiB RAM.
Each variant started with empty project dependencies and separate empty XDG_CACHE_HOME, MATHLIB_CACHE_DIR, and LAKE_CACHE_DIR.
The Lean toolchain was already installed.
Packages ran in this order: common, KV, consistency, disaster recovery, consensus.
For each package, dependency setup was followed by lake build.
Variants ran sequentially rather than concurrently.

Metric	Baseline: unrestricted fetch, separate dependencies	Selective fetch only	Selective fetch + shared dependencies
Dependency setup	424.1 s	378.9 s	129.8 s
First builds	325.8 s	396.2 s	462.1 s
Setup + first builds	750.0 s	775.1 s	591.9 s
Total change against baseline	-	3.4% slower	21.1% faster
Built lean/ tree	36.790 GiB	6.104 GiB	1.781 GiB
Dependency directories after builds	36.234 GiB	5.548 GiB	1.227 GiB
Mathlib compressed cache directory	452.1 MiB	67.7 MiB	67.7 MiB
Retained .ltar cache files	9,031	827	827

Dependency setup includes materializing/cloning packages, compiling the Mathlib cache executable, and fetching/unpacking the cache.
The time totals sum the timed commands; they exclude disk-measurement overhead.
Disk figures use allocated bytes from du -s -B1 and were recorded before additional validation.
Compressed cache sizes are disk measurements, not measurements of total network traffic; Git dependency downloads are additional.

Together, the changes reduced dependency setup by 69.4%, setup plus first builds by 21.1%, and built-tree disk use by 95.2% in this run.
Selective fetching alone substantially reduced disk use but did not demonstrate an end-to-end speed improvement.
Native build timings varied considerably despite unchanged sources, including a 332 s first KV build in the shared run versus 144 s in the baseline.
This was one pass per variant on a shared machine, without OS page-cache flushing or statistical repetitions, so these timing differences are indicative rather than causal estimates or guarantees.

Cache-path compatibility finding

Changing packagesDir alone is not enough with the pinned Mathlib cache tool.
Mathlib's own archives are redirected to its resolved directory, but other dependencies' archives use embedded paths beneath .lake/packages.
Without the compatibility links, Batteries artifacts landed outside the configured shared dependency tree and the common first build rebuilt Batteries from source, taking 161.4 s.
That exploratory attempt was stopped and excluded from the comparison.
The shared measurement was restarted from a fresh snapshot and empty caches with the links present; its common first build took 7.8 s.

Detailed impact on CI performance

Where this helps

The Lean workflow has five isolated package jobs and three independent trace-replay jobs.
All eight switch from an unrestricted Mathlib cache fetch to fetching the required module closure.

CI surface	Expected effect	What does not change
Five package jobs, cold dependency-cache miss	Fewer upstream cache archives downloaded/unpacked and a much smaller dependency tree to save to Actions cache	Each job still independently materializes its Git dependencies and builds the cache tool
Five package jobs, warm dependency-cache hit	Smaller Actions archives should reduce restore I/O, runner disk use, and save I/O when a new key is populated	The setup step and independent kernel/axiom checks still run
Consensus, KV, and consistency replay jobs	Selective upstream cache download/unpacking instead of fetching all Mathlib	They still build their own replayer and depend on their corresponding trace-capture job
Native CCF trace-capture jobs	No intended performance change	C++ builds and trace generation are unchanged
ACI Genoa recovery-replayer build in ci.yml	No targeted cache-fetch optimization in this change	It still directly builds its existing replayer target
Documentation recovery-viewer build	No targeted cache-fetch optimization in this change	Its existing replayer build path is unchanged

The strongest expected CI benefit is smaller dependency download/cache archives and less archive I/O, not faster proof checking.
Actual Actions archive sizes and transfer times still need measurement: the local compressed Mathlib cache directory is not the Actions cache archive, which also includes Git checkouts and native build outputs.

Why the local 21% result is not a CI prediction

The local benchmark builds all five packages in one checkout.
Its shared directory avoids repeated Git materialization, repeated compilation of the Mathlib cache executable, and some repeated dependency compilation across packages.
Separate CI jobs have separate filesystems and containers.
Changing their dependency directory does not make one job reuse another job's checkout or compiled dependencies.
Package caches remain keyed by package and architecture, and replay jobs remain independent.
This PR does not introduce a dependency-preparation job, cross-job artifact reuse, a shared mutable directory between jobs, or replay-binary transfer.
Those would be separate workflow changes.

Consequently, do not apply the 69% local setup reduction or 21% local total reduction to the parallel CI workflow.
The selective-only local result also shows why reducing download/disk footprint alone does not establish a total-time improvement.
No new GitHub Actions before/after timings are claimed here.

Work that remains unchanged

Selective fetching changes which unused prebuilt files are downloaded, not the modules actually imported by the specifications.
Mathlib remains in the checked import closures.
lake check still exports and independently rechecks those declarations and audits their axioms.
The native modules needed by replay executables still need to be compiled/linked.
The existing package check targets, test roots, lint drivers, and axiom policy remain unchanged.

Unlike removing Mathlib, this does not remove its imported environment from kernel rechecking.
It should not be expected to reproduce the proof-checking or native-linking reductions reported by #8702.

Cold/warm comparison and follow-up measurement

The v3 key and changed dependency configuration deliberately invalidate the old, oversized caches.
The first successful run will pay cold setup and archive-upload costs.
It should not be compared directly with a warm-cache baseline as a steady-state result.

Before calling this a CI speedup, compare:

1. A cold run at this head with cache-hit status recorded.
2. A rerun of the same head after caches are populated.
3. Multiple successful main-branch runs on the same runner pools, container versions, and architecture.

Record dependency-cache restore/save durations and bytes, selective Mathlib fetch duration and requested-module counts, build/kernel/axiom step duration, replay build duration, total job-seconds across the eight jobs, and the workflow's longest dependency path separately.
Also record toolchain installation, container/package-manager time, runner queue time, and native capture variation so unrelated variation is not attributed to this change.
Proof-only edits should retain the module-list hash; changing direct imports should invalidate the corresponding selective cache without requiring a Mathlib version bump.

Migration and limitations

For an existing checkout, move the old package-local .lake/packages directories aside before running the helper.
It refuses to overwrite/delete an existing directory or replace a symlink pointing elsewhere.
All five packages must keep compatible dependency pins, and setup/build/update commands sharing one dependency tree must run sequentially.
Fresh CI checkouts and the new cache namespace do not require manual migration.

Validation

Passed locally using the implemented helper:

• python3 tests/lean_setup_test.py: 10 regression tests, covering module discovery, lint dependencies, generated-directory exclusion, repeat setup, shared links, non-destructive migration failures, invalid inputs, Lake error propagation, side-effect-free module listing, and import-sensitive/proof-insensitive cache identity.
• For all five packages: selective setup, lake build --wfail --fail-fast, lake exe check-imports, the common-library build needed for downstream linting, and lake lint.
• KV replay fixtures: 72/72; disaster-recovery replay fixtures: 419/419.
• All 25 consistency and 8 consensus valid/invalid fixture commands returned their expected statuses.
• cd lean/common && lake check --inadvisably-no-sandbox: independent kernel and axiom check passed.
• All five real module lists match the measured benchmark lists; all manifests differ only in packagesDir; no Lean sources changed.
• ShellCheck, Black, Ruff, whitespace, ASCII policy, documentation-newline, Prettier, copyright, and the other available repository checks passed.

Full local validation is not claimed:

• scripts/ci-checks.sh was run without auto-fix. After restoring the missing uv tool and formatting only the new test file, 15 of its 16 checks passed. The sole remaining blocker is scripts/test-buckets-checks.sh: cmake: command not found. The bucket inventory still needs checking in the configured C++ build environment.
• sphinx-build --fail-on-warning -b html doc doc/html was attempted after installing the documented documentation requirements in an isolated virtual environment. It is blocked by FileNotFoundError: 'doxygen'. A full documentation build still needs the documentation build prerequisites.
• Independent kernel/axiom checks for the other four packages and required GitHub Actions checks remain for CI. No checks were disabled or weakened to obtain a pass.

[Heidi Howard (heidihoward)]

Closing as we are doing #8702 instead