From 78c3ad8104c6cc893da4a4f334c2175c21bb01c6 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 14 Nov 2026 13:33:53 -0800 Subject: [PATCH 1/3] Slim Lake setup files before CI caches and validates the pool build Lake writes a .setup.json compiler input per module listing absolute artifact paths for every transitive import (~1.6 MB each, 46 GB of the 69 GB pool build). Lake never reads them back, and the validation cache and exposition extractor only use keys naming local modules. Drop the other keys after every CI build step so restores, saves, uploads, and lint/quality fingerprinting stop handling the dead weight. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean_action_ci.yml | 24 ++++++ python/ci-performance.md | 17 ++++ python/lean_pool/slim_setup.py | 122 +++++++++++++++++++++++++++ python/tests/test_slim_setup.py | 119 ++++++++++++++++++++++++++ 4 files changed, 282 insertions(+) create mode 100644 python/lean_pool/slim_setup.py create mode 100644 python/tests/test_slim_setup.py diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 8f38e7298d..798622b5f0 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -404,6 +404,12 @@ jobs: --log lean-build.log --base "$time_base" fi + # Lake writes setup files only as compiler inputs, each listing every + # transitive import (~1.6 MB; ~46 GB pool-wide). Before validating, + # caching, or uploading, keep just the local entries our readers use. + - name: Slim Lake setup files + run: PYTHONPATH=python python3 -m lean_pool.slim_setup + # Main publishes the shared full build. A minimal-verifier PR publishes # only its own projects; the verifier overlays them on the main cache. # A cold merge-queue build publishes it too, for main to restore. @@ -648,6 +654,12 @@ jobs: --log shard-build.log --base "$time_base" --modules $modules fi + # Lake writes setup files only as compiler inputs, each listing every + # transitive import (~1.6 MB; ~46 GB pool-wide). Before validating, + # caching, or uploading, keep just the local entries our readers use. + - name: Slim Lake setup files + run: PYTHONPATH=python python3 -m lean_pool.slim_setup + # Ship only what this build produced; unchanged (cache-replayed) # files stay out, so `finalize` can layer the shard outputs onto the # same restored cache without clobbering anything fresher. @@ -833,6 +845,12 @@ jobs: --log lean-build.log --base "$time_base" --exclude-projects $SHARD_PROJECTS fi + # Lake writes setup files only as compiler inputs, each listing every + # transitive import (~1.6 MB; ~46 GB pool-wide). Before validating, + # caching, or uploading, keep just the local entries our readers use. + - name: Slim Lake setup files + run: PYTHONPATH=python python3 -m lean_pool.slim_setup + # Main publishes the shared full build. A minimal-verifier PR publishes # only its own projects; the verifier overlays them on the main cache. # A cold merge-queue build publishes it too, for main to restore. @@ -1096,6 +1114,12 @@ jobs: --log lean-build.log --base "$time_base" fi + # Lake writes setup files only as compiler inputs, each listing every + # transitive import (~1.6 MB; ~46 GB pool-wide). Before validating, + # caching, or uploading, keep just the local entries our readers use. + - name: Slim Lake setup files + run: PYTHONPATH=python python3 -m lean_pool.slim_setup + - name: Install validation dependencies run: cd python && uv sync --locked diff --git a/python/ci-performance.md b/python/ci-performance.md index 19beaf6e62..59071f260a 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -19,6 +19,23 @@ its key. All consumers use the same paths and compatibility keys. Preflight and Mathlib documentation restore only dependencies. Existing `Lake-` caches expire normally; the first run after this migration must seed the new namespaces. +### Slim Lake setup files + +Before compiling a module, Lake writes `.lake/build/ir/.setup.json` for +`lean --setup`. Its `importArts` field lists the absolute artifact paths of every +transitive import, so a module that imports Mathlib carries about 3,000 entries +(about 1.6 MB). On November 14, 2026 these files were 46 GB of a 69 GB pool build. +Every job wrote them out on cache restore, hauled them through cache saves and +artifact uploads, and JSON-parsed them during the lint and quality steps, where +that parsing accounted for most of their time. + +Lake never reads a setup file back; it rewrites one when it recompiles that +module. The only readers, `validation_cache` and the exposition extractor, use +just the `importArts` keys that name a `LeanPool` module or a Lean source in the +checkout. So every CI build step is followed by +`python3 -m lean_pool.slim_setup`, which drops the other keys and keeps +modification times, so shard packaging still ships only fresh files. + Documentation retains its separate, integrity-checked SQLite checkpoints. They still depend on available cache capacity; this change reduces duplicate data instead of changing the repository's paid storage limit. diff --git a/python/lean_pool/slim_setup.py b/python/lean_pool/slim_setup.py new file mode 100644 index 0000000000..0b840e0fab --- /dev/null +++ b/python/lean_pool/slim_setup.py @@ -0,0 +1,122 @@ +"""Shrink Lake's per-module ``.setup.json`` compiler inputs to local imports. + +Before compiling a module, Lake writes ``.lake/build/ir/.setup.json`` +and passes it to ``lean --setup``. Its ``importArts`` field records absolute +artifact paths for every transitive import, so a module that imports Mathlib +carries about 3,000 entries (~1.6 MB). Across the pool that is ~46 GB of the +~69 GB build directory that every CI job restores, saves, and uploads. + +Lake never reads these files back: it rewrites one whenever it recompiles that +module. Lean Pool's own readers (``validation_cache`` and the exposition +extractor) only use ``importArts`` keys that name a ``LeanPool`` module or a +Lean source in this checkout. Dropping every other key keeps their results +unchanged. Modification times are preserved, so ``find -newer`` packaging still +ships only freshly built files. Standard library only, so CI can run it with +the runner's ``python3``. +""" + +from __future__ import annotations + +import argparse +import json +import logging +import os +import sys +from concurrent.futures import ProcessPoolExecutor +from dataclasses import dataclass +from pathlib import Path + +LOGGER = logging.getLogger(__name__) +SETUP_SUFFIX = ".setup.json" + + +@dataclass(frozen=True) +class Outcome: + """Sizes of one setup file before and after slimming.""" + + before: int + after: int + rewritten: bool + + +def is_local(module: str, root: Path) -> bool: + """Whether a reader of the inventory could map ``module`` to a pool source.""" + return ( + module.split(".")[0] == "LeanPool" + or (root / (module.replace(".", "/") + ".lean")).is_file() + ) + + +def slim_inventory(inventory: dict, root: Path) -> dict | None: + """Return the inventory without non-local imports, or ``None`` if unchanged.""" + imports = inventory.get("importArts") + if not isinstance(imports, dict): + return None + kept = {module: arts for module, arts in imports.items() if is_local(module, root)} + if len(kept) == len(imports): + return None + return inventory | {"importArts": kept} + + +def slim_file(path: Path, root: Path) -> Outcome: + """Rewrite one setup file in place, keeping its access and modification times.""" + status = path.stat() + try: + slimmed = slim_inventory(json.loads(path.read_bytes()), root) + except (OSError, ValueError) as error: + LOGGER.warning("%s: left unchanged (%s)", path, error) + return Outcome(status.st_size, status.st_size, rewritten=False) + if slimmed is None: + return Outcome(status.st_size, status.st_size, rewritten=False) + temporary = path.with_name(path.name + ".slim") + after = temporary.write_bytes(json.dumps(slimmed, separators=(",", ":")).encode()) + os.utime(temporary, ns=(status.st_atime_ns, status.st_mtime_ns)) + temporary.replace(path) + return Outcome(status.st_size, after, rewritten=True) + + +def setup_files(build: Path) -> list[Path]: + """Every Lake setup file under the build's ``ir`` directory.""" + directory = build / "ir" + if not directory.is_dir(): + return [] + return sorted(directory.rglob("*" + SETUP_SUFFIX)) + + +def _slim_in_worker(arguments: tuple[Path, Path]) -> Outcome: + return slim_file(*arguments) + + +def slim_build(root: Path, workers: int | None = None) -> list[Outcome]: + """Slim every setup file in ``root``'s pool build, in parallel.""" + paths = setup_files(root / ".lake/build") + if not paths: + return [] + with ProcessPoolExecutor(max_workers=workers or os.cpu_count()) as executor: + return list( + executor.map( + _slim_in_worker, [(path, root) for path in paths], chunksize=64 + ) + ) + + +def main(arguments: list[str] | None = None) -> int: + """Slim the checkout's setup files and report the space saved.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=Path.cwd()) + parser.add_argument("--workers", type=int) + options = parser.parse_args(arguments) + logging.basicConfig(level=logging.INFO, format="slim-setup: %(message)s") + outcomes = slim_build(options.repo.resolve(), options.workers) + before = sum(outcome.before for outcome in outcomes) + after = sum(outcome.after for outcome in outcomes) + rewritten = sum(outcome.rewritten for outcome in outcomes) + print( + f"Slimmed {rewritten} of {len(outcomes)} Lake setup files: " + f"{before / 1e9:.2f} GB -> {after / 1e9:.2f} GB." + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/python/tests/test_slim_setup.py b/python/tests/test_slim_setup.py new file mode 100644 index 0000000000..4554fcebcd --- /dev/null +++ b/python/tests/test_slim_setup.py @@ -0,0 +1,119 @@ +"""Check that slimming Lake setup files keeps every local reader's result.""" + +from __future__ import annotations + +import json +import os +from pathlib import Path + +import pytest + +from lean_pool.exposition.extract import project_sources +from lean_pool.slim_setup import main, slim_build, slim_file +from lean_pool.validation_cache import source_inventory + +ARTS = [["/runner/.lake/build/lib/lean/X.olean"], ["/runner/.lake/build/ir/X.ir"]] +IMPORTS = ( + "Init.Prelude", + "Mathlib.Order.Basic", + "LeanPool.A.Detail", + "LeanPool.Gone", + "Local.Helper", +) + + +def _setup_path(root: Path, module: str) -> Path: + return root / (".lake/build/ir/" + module.replace(".", "/") + ".setup.json") + + +@pytest.fixture +def repository(tmp_path: Path) -> Path: + """A pool project importing Mathlib, a pool module, and a non-pool local file.""" + for module in ("LeanPool", "LeanPool.A", "LeanPool.A.Detail", "Local.Helper"): + path = tmp_path / (module.replace(".", "/") + ".lean") + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(f"-- {module}\n") + setup = _setup_path(tmp_path, "LeanPool.A") + setup.parent.mkdir(parents=True, exist_ok=True) + setup.write_text( + json.dumps( + { + "name": "LeanPool.A", + "isModule": True, + "importArts": dict.fromkeys(IMPORTS, ARTS), + }, + indent=2, + ) + ) + os.utime(setup, ns=(1_000_000_000, 2_000_000_000)) + return tmp_path + + +def _readers(root: Path) -> tuple[set[Path], set[Path]]: + validation = source_inventory(root, ["LeanPool.A"]) + exposition = project_sources(root, "A") + return validation, exposition + + +def test_slimming_keeps_only_local_imports(repository: Path) -> None: + """Dependency entries go; pool modules and checkout sources stay.""" + setup = _setup_path(repository, "LeanPool.A") + outcome = slim_file(setup, repository) + inventory = json.loads(setup.read_text()) + assert outcome.rewritten and outcome.after < outcome.before + assert list(inventory["importArts"]) == [ + "LeanPool.A.Detail", + "LeanPool.Gone", + "Local.Helper", + ] + assert inventory["importArts"]["Local.Helper"] == ARTS + assert inventory["name"] == "LeanPool.A" and inventory["isModule"] is True + + +def test_readers_see_the_same_sources(repository: Path) -> None: + """Validation and exposition inventories, including errors, are unchanged.""" + inventory = json.loads(_setup_path(repository, "LeanPool.A").read_text()) + del inventory["importArts"]["LeanPool.Gone"] + _setup_path(repository, "LeanPool.A").write_text(json.dumps(inventory)) + before = _readers(repository) + slim_build(repository, workers=1) + assert _readers(repository) == before + assert repository / "Local/Helper.lean" in before[0] + + +def test_modification_time_is_preserved(repository: Path) -> None: + """Shard packaging selects files by mtime, so slimming must not touch it.""" + setup = _setup_path(repository, "LeanPool.A") + slim_file(setup, repository) + assert setup.stat().st_mtime_ns == 2_000_000_000 + assert not setup.with_name(setup.name + ".slim").exists() + + +def test_slimming_is_idempotent(repository: Path) -> None: + """A second pass finds nothing to drop and leaves the file alone.""" + setup = _setup_path(repository, "LeanPool.A") + slim_file(setup, repository) + content = setup.read_bytes() + assert not slim_file(setup, repository).rewritten + assert setup.read_bytes() == content + + +def test_unreadable_files_are_left_alone(repository: Path) -> None: + """A truncated file stays as it is; readers already fall back on it.""" + setup = _setup_path(repository, "LeanPool.A") + setup.write_text("{") + assert not slim_file(setup, repository).rewritten + assert setup.read_text() == "{" + + +def test_command_reports_savings( + repository: Path, capsys: pytest.CaptureFixture[str] +) -> None: + """The CLI slims the whole build and prints a one-line summary.""" + assert main(["--repo", str(repository), "--workers", "1"]) == 0 + assert "Slimmed 1 of 1 Lake setup files" in capsys.readouterr().out + + +def test_missing_build_is_a_no_op(tmp_path: Path) -> None: + """Jobs that restored nothing still succeed.""" + assert slim_build(tmp_path) == [] From 103fe79d12817bf35ece29fbd69a5ff973411ca8 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 14 Nov 2026 13:39:19 -0800 Subject: [PATCH 2/3] Drop artifact paths from slimmed setup files Both readers use only import names, and big projects list hundreds of local imports with four absolute paths each (4.8 GB pool-wide). Co-Authored-By: Claude Opus 5.5 --- python/ci-performance.md | 5 +++-- python/lean_pool/slim_setup.py | 14 +++++++------- python/tests/test_slim_setup.py | 4 ++-- 3 files changed, 12 insertions(+), 11 deletions(-) diff --git a/python/ci-performance.md b/python/ci-performance.md index 59071f260a..2d0b8455af 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -32,8 +32,9 @@ that parsing accounted for most of their time. Lake never reads a setup file back; it rewrites one when it recompiles that module. The only readers, `validation_cache` and the exposition extractor, use just the `importArts` keys that name a `LeanPool` module or a Lean source in the -checkout. So every CI build step is followed by -`python3 -m lean_pool.slim_setup`, which drops the other keys and keeps +checkout, never the artifact paths. So every CI build step is followed by +`python3 -m lean_pool.slim_setup`, which keeps only those names, with empty +artifact lists, and preserves modification times, so shard packaging still ships only fresh files. Documentation retains its separate, integrity-checked SQLite checkpoints. They diff --git a/python/lean_pool/slim_setup.py b/python/lean_pool/slim_setup.py index 0b840e0fab..f935bdb05a 100644 --- a/python/lean_pool/slim_setup.py +++ b/python/lean_pool/slim_setup.py @@ -9,10 +9,10 @@ Lake never reads these files back: it rewrites one whenever it recompiles that module. Lean Pool's own readers (``validation_cache`` and the exposition extractor) only use ``importArts`` keys that name a ``LeanPool`` module or a -Lean source in this checkout. Dropping every other key keeps their results -unchanged. Modification times are preserved, so ``find -newer`` packaging still -ships only freshly built files. Standard library only, so CI can run it with -the runner's ``python3``. +Lean source in this checkout, never the artifact paths. Keeping just those keys, +with empty artifact lists, leaves their results unchanged. Modification times +are preserved, so ``find -newer`` packaging still ships only freshly built +files. Standard library only, so CI can run it with the runner's ``python3``. """ from __future__ import annotations @@ -48,12 +48,12 @@ def is_local(module: str, root: Path) -> bool: def slim_inventory(inventory: dict, root: Path) -> dict | None: - """Return the inventory without non-local imports, or ``None`` if unchanged.""" + """Return local import names without artifacts, or ``None`` if unchanged.""" imports = inventory.get("importArts") if not isinstance(imports, dict): return None - kept = {module: arts for module, arts in imports.items() if is_local(module, root)} - if len(kept) == len(imports): + kept = {module: [] for module in imports if is_local(module, root)} + if kept == imports: return None return inventory | {"importArts": kept} diff --git a/python/tests/test_slim_setup.py b/python/tests/test_slim_setup.py index 4554fcebcd..28be249039 100644 --- a/python/tests/test_slim_setup.py +++ b/python/tests/test_slim_setup.py @@ -56,7 +56,7 @@ def _readers(root: Path) -> tuple[set[Path], set[Path]]: def test_slimming_keeps_only_local_imports(repository: Path) -> None: - """Dependency entries go; pool modules and checkout sources stay.""" + """Dependency entries and artifact paths go; local import names stay.""" setup = _setup_path(repository, "LeanPool.A") outcome = slim_file(setup, repository) inventory = json.loads(setup.read_text()) @@ -66,7 +66,7 @@ def test_slimming_keeps_only_local_imports(repository: Path) -> None: "LeanPool.Gone", "Local.Helper", ] - assert inventory["importArts"]["Local.Helper"] == ARTS + assert inventory["importArts"]["Local.Helper"] == [] assert inventory["name"] == "LeanPool.A" and inventory["isModule"] is True From e4934b4cc1a8f3ab6e1c8d768fa59cad382ae692 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 14 Nov 2026 13:43:44 -0800 Subject: [PATCH 3/3] Test that Lake replays and rebuilds correctly after slimming Runs under the pinned-Lean CI step so a toolchain bump that starts reading setup files back fails loudly. Co-Authored-By: Claude Opus 5.5 --- python/tests/test_ci_pr_build.py | 29 ++++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/python/tests/test_ci_pr_build.py b/python/tests/test_ci_pr_build.py index ce09ca06e4..a833cd4bfe 100644 --- a/python/tests/test_ci_pr_build.py +++ b/python/tests/test_ci_pr_build.py @@ -13,7 +13,7 @@ import pytest -from lean_pool import ci_artifacts, ci_pr_build, rebase_fastpath +from lean_pool import ci_artifacts, ci_pr_build, rebase_fastpath, slim_setup TOOLCHAIN = (Path(__file__).resolve().parents[2] / "lean-toolchain").read_text().strip() @@ -332,6 +332,33 @@ def test_lake_rebuilds_changed_dependency_and_rejects_invalid_proof( assert "rfl" in result.stdout + result.stderr +def test_lake_replays_and_rebuilds_after_setup_files_are_slimmed(repository): + """Slimmed compiler inputs neither force rebuilds nor hide a changed import.""" + root, _, _ = repository + lake = _lake() + subprocess.run( + [str(lake), "build", "LeanPool.B"], cwd=root, check=True, capture_output=True + ) + assert any(outcome.rewritten for outcome in slim_setup.slim_build(root, 1)) + setup = json.loads((root / ".lake/build/ir/LeanPool/B.setup.json").read_text()) + assert setup["importArts"] == {"LeanPool.A": []} + replay = subprocess.run( + [str(lake), "build", "--no-build", "LeanPool.B"], + cwd=root, + capture_output=True, + text=True, + ) + assert replay.returncode == 0, replay.stdout + replay.stderr + (root / "LeanPool/A.lean").write_text( + "module\n@[expose] public def value : Nat := 2\n" + ) + result = subprocess.run( + [str(lake), "build", "LeanPool.B"], cwd=root, capture_output=True, text=True + ) + assert result.returncode != 0 + assert "rfl" in result.stdout + result.stderr + + def test_lake_keeps_unchanged_proof_after_metadata_edit(repository, monkeypatch): """Lake accepts matching artifacts without recompiling unchanged proofs.""" root, base, previous = repository