[Vilin97]

Why

Before compiling a module, Lake writes .lake/build/ir/<Module>.setup.json for lean --setup. Its importArts lists the absolute artifact paths of every transitive import: about 3,000 entries, roughly 1.6 MB, per Mathlib-importing module. On the Azure VM's current pool build these files are 49 GB of 69 GB, while the oleans are 22 GB.

Every CI job pays for this:

• Cache restore (4–8 min per job) unpacks all of it.
• Save pool build (~5 min) and Package build for documentation (~5 min) haul it around.
• Lint and quality spend most of their time JSON-parsing it while fingerprinting cache hits. A VM profile of ValidationCache.fingerprint over all units took 444 s: 280 s in read + json on setup files, against 14 s to hash the 611 MB of sources.

Lake never reads a setup file back. It rewrites one when it recompiles that module, as Lake/Build/Actions.lean shows. The only readers are validation_cache._module_sources and exposition.extract.project_sources. Both use only importArts keys that name a LeanPool module or a Lean source in the checkout, and never the artifact paths.

What

• New python/lean_pool/slim_setup.py (stdlib only, parallel). It rewrites each setup file to keep only those local import names, with empty artifact lists, and preserves mtimes so the shards' find -newer packaging still ships only fresh files. Unreadable files are left alone.
• A Slim Lake setup files step after every build step in lean_action_ci.yml: single build, shard, finalize, and rebase. It runs before validation, docs packaging, artifact uploads and cache saves.
• Tests in python/tests/test_slim_setup.py. They check that both readers return identical results before and after, plus mtime preservation, idempotence, unreadable files, and the CLI.
• A note in python/ci-performance.md.

No check changes what it accepts. The validation fingerprints hash the same source set, so existing receipts stay valid.

Verification (Azure VM, v4.35.0, pool at 5dd7126)

• Lake still sees the build as up to date. After building LeanPool.Champernowne and slimming, lake build --no-build reports "All targets up-to-date" (exit 0), and a normal lake build recompiles nothing. After editing a source, Lake rebuilds that module normally.
• Inventories are unchanged pool-wide. I slimmed all 31,455 setup files from the full pool build, then compared source_inventory for all 343 validation units: 0 differences. With the final names-only format the setup files shrink from 49.0 GB to 0.63 GB (78×), and building the inventories drops from 487 s to 49 s.
• pytest for slim_setup, validation_cache and exposition_extract passes, and ruff is clean.

Rollout

The first run after merge still restores the existing full-size cache and pays a one-time slimming pass: about 7 min with 4 workers on the busy VM. Main's next cache save is slim, and later restores benefit from then on.

🤖 Generated with Claude Code

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium impact] The PR appears safe to merge, with the previous test-coverage gap addressed.

Summary

The PR shrinks Lake setup files before CI validates, packages, or caches build outputs.

• CI trims Lake setup files before it caches and shares builds.

_{Reviews (2) · Last reviewed commit: "Test that Lake replays and rebuilds corr..." · Reviewed by Greptile}

[Vilin97]

Names-only slimming, measured pool-wide on the Azure VM (31,455 setup files, pool at 5dd7126):

• Setup files: 49.0 GB → 0.63 GB
• source_inventory for all 343 validation units: 487 s from the original files, 49 s from the slimmed ones, with 0 differences
• One-time slimming of a full-size build: 408 s with 4 workers on the busy VM (load ~35 on 16 cores). This only happens on the first restore of today's cache.

🤖 Generated with Claude Code

[Vilin97]

Source review passes at e4934b4cc1a8f3ab6e1c8d768fa59cad382ae692; protected validation and separate workflow-change authorization remain outstanding.

The slimmer retains local import names, including missing LeanPool names needed for failure detection, and preserves modification times before atomic replacement. The validation and exposition readers consume those retained names rather than the removed artifact-path payloads. The new pinned-Lake regression checks both unchanged replay and rebuilding after an imported source changes; it addresses the previous inline review's concrete coverage request. I found no actionable defect in the five-file change.

Hosted Python and workflow checks passed in the saved intake. Core was still running, so the real pinned-toolchain regression and full build outcome remain to be verified. The measured VM savings are author claims, not independent evidence here. This PR changes four Lean CI steps and cache inputs; the repository's separate workflow-change authorization requirement still applies, and the current operative authorization names PR758, PR817 and PR819 rather than this PR. No queue or auto-merge action is taken.