Slim Lake setup files before CI caches and validates the pool build

.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
 

python/ci-performance.md

@@ -19,6 +19,24 @@ 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/<Module>.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, 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
 still depend on available cache capacity; this change reduces duplicate data
 instead of changing the repository's paid storage limit.

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/<Module>.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, 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
+
+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 local import names without artifacts, or ``None`` if unchanged."""
+    imports = inventory.get("importArts")
+    if not isinstance(imports, dict):
+        return None
+    kept = {module: [] for module in imports if is_local(module, root)}
+    if kept == 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())

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

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 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())
+    assert outcome.rewritten and outcome.after < outcome.before
+    assert list(inventory["importArts"]) == [
+        "LeanPool.A.Detail",
+        "LeanPool.Gone",
+        "Local.Helper",
+    ]
+    assert inventory["importArts"]["Local.Helper"] == []
+    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) == []