From 78c3ad8104c6cc893da4a4f334c2175c21bb01c6 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 14 Nov 2026 13:33:53 -0800 Subject: [PATCH 1/7] 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/7] 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/7] 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 From 53136ced9414a8de0c0b26cd6ec007d78d29b861 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 14 Nov 2026 14:42:15 -0800 Subject: [PATCH 4/7] Recompile only what a PR push changed, and measure changes from current main The build-time gate deleted the output of every file a PR changed relative to main so each run would time it afresh. A PR adding a 1,300-file project recompiled all of it on every push, in the merge queue, and on main. - build_time_limits: `check` writes a per-module timing receipt bound to a hash of the module's .olean outputs; `prepare` only invalidates changed modules without a matching receipt; `check` judges the recorded time of reused output against the limit. Untimed output is still always rebuilt. - ci_pr_build / rebase_fastpath: restore the unchanged-source modules of the PR's newest successful run instead of requiring identical sources; Lake's traces decide what is still valid. Shards restore them too. - Workflow: measure a PR's changes from the tested merge commit's first parent. The event's base.sha can trail main by days, which made every project merged since count as changed and be rebuilt. Co-Authored-By: Claude Fable 5.2 --- .github/CODE_QUALITY.md | 23 ++-- .github/workflows/lean_action_ci.yml | 71 +++++++++--- python/ci-performance.md | 19 ++++ python/lean_pool/build_time_limits.py | 146 ++++++++++++++++++++----- python/lean_pool/ci_pr_build.py | 29 ++++- python/lean_pool/rebase_fastpath.py | 48 +++++++- python/tests/test_build_time_limits.py | 121 +++++++++++++++++++- python/tests/test_ci_cache_contract.py | 11 +- python/tests/test_ci_pr_build.py | 119 ++++++++++++++++++-- 9 files changed, 511 insertions(+), 76 deletions(-) diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index d34c4517e0..1e0b1b5dd0 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -32,20 +32,29 @@ After the build, it reads Lake's per-module times from the log and fails when a the PR adds or modifies took more than 600 s. Times are Lake's wall-clock times on GitHub's 4-vCPU runners. Existing files are checked only once a PR changes them. -After all cache and artifact restores, `prepare` removes the compiled outputs -of the added or modified modules that job is responsible for timing. This happens -even for a cache produced under the same policy: an untouched file in that cache -need not have passed the changed-file limit. Each changed module must emit a -fresh successful build timing in its responsible job; missing timings and cache -replays fail that check. +`check` records each changed module's time in a receipt next to its compiled +output (`.timing.json`), bound to a hash of that output's `.olean` files. +After all cache and artifact restores, `prepare` removes the compiled outputs of +every added or modified module the job is responsible for whose output has no +matching receipt. So output that was compiled without being timed is always +rebuilt, even from a cache produced under the same policy: an untouched file in +that cache need not have passed the changed-file limit. Each changed module must +then have either a fresh successful build timing from its responsible job or the +recorded time of the exact output being reused; that time is checked against the +limit either way, and a module with neither fails the check. Shards check their assigned modules. Assembly excludes projects listed in the same run's shard matrix and checks all remaining changed modules; the canonical gate requires every shard and assembly to succeed. Single and rebased root builds check all changed modules. Untouched modules can still reuse compiled output. +"Changed" is measured from the main commit the run is tested against: the tested +merge commit's first parent for a PR, not the event's `base.sha`, which can trail +main and would count projects merged since as the PR's own. + +A later push to a PR restores the outputs of modules whose own source is unchanged +from that PR's newest successful run; Lake's traces decide which are still valid. Reused PR, rebase and queue artifacts must still match `build_time_limits.py`. -That match does not replace the fresh timing required for a changed module. The Lean workflow runs on Lean, Lake, project metadata, quality-checker, and workflow changes. It restores and saves Lake caches and pulls Mathlib oleans with `lake exe cache get` when the cache is cold. diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 798622b5f0..eeae274f49 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -97,6 +97,7 @@ jobs: reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }} previous_head: ${{ steps.plan.outputs.previous_head }} queue_build: ${{ steps.plan.outputs.queue_build }} + diff_base: ${{ steps.plan.outputs.diff_base }} steps: - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd @@ -162,14 +163,24 @@ jobs: # exceeds the kernel's 128 KiB limit on a single environment string. changed_files="$RUNNER_TEMP/changed-files.txt" : > "$changed_files" + # The revision this run's own changes are measured from, for the plan + # and for every job's build-time gate. + diff_base="$BASE_SHA" case "$EVENT_NAME" in merge_group) git diff --name-only --no-renames "$BASE_SHA"..HEAD > "$changed_files" ;; pull_request) - git diff --name-only --no-renames "$BASE_SHA"...HEAD > "$changed_files" + # The event's base.sha can trail main by days, which would count + # everything main merged since as this PR's change. The tested + # merge commit's first parent is the main tip it merges into. + if [ "$(git rev-parse -q --verify 'HEAD^2' || true)" = "$PR_HEAD" ]; then + diff_base=$(git rev-parse 'HEAD^1') + fi + git diff --name-only --no-renames "$diff_base"...HEAD > "$changed_files" ;; push) + diff_base="$BEFORE_SHA" if [ -n "$BEFORE_SHA" ] \ && ! printf '%s' "$BEFORE_SHA" | grep -q '^0*$' \ && git cat-file -e "$BEFORE_SHA" 2>/dev/null; then @@ -182,6 +193,7 @@ jobs: diff_available=false ;; esac + echo "diff_base=$diff_base" >> "$GITHUB_OUTPUT" minimal_build=false if [ "$EVENT_NAME" = pull_request ] && grep -Eq '^(python/lean_pool/(exposition/|ci_artifacts.py$)|scripts/exposition/|.github/workflows/exposition-verify.yml$)' "$changed_files"; then minimal_build=true @@ -382,12 +394,13 @@ jobs: - name: Build project id: compilation env: - BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }} + BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }} run: | set -euo pipefail - # Always rebuild this job's changed files after every cache/artifact - # restore. A same-policy cache need not have timed them while changed. - # `check` requires fresh timings; `watch` retains the 60-minute limit. + # After every cache/artifact restore, `prepare` forces a rebuild of + # each changed file whose restored output has no recorded build time, + # so `check` judges a time measured in CI for every changed file. + # `watch` retains the 60-minute limit. time_base="" if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \ && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then @@ -615,10 +628,31 @@ jobs: echo "Mathlib already present from cache" fi + - name: Install uv + if: github.event_name == 'pull_request' + uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff + with: + enable-cache: true + + - name: Reuse compiled files from this PR's successful runs + if: github.event_name == 'pull_request' && steps.cache.outputs.cache-hit != 'true' + continue-on-error: true + env: + GH_TOKEN: ${{ github.token }} + PR_NUMBER: ${{ github.event.pull_request.number }} + PR_BRANCH: ${{ github.head_ref }} + PR_HEAD: ${{ github.event.pull_request.head.sha }} + PR_BASE: ${{ github.event.pull_request.base.sha }} + CURRENT_RUN: ${{ github.run_id }} + run: >- + PYTHONPATH=python uv run --project python --locked python -m lean_pool.ci_pr_build + --number "$PR_NUMBER" --branch "$PR_BRANCH" + --head "$PR_HEAD" --base "$PR_BASE" --current-run "$CURRENT_RUN" + - name: Build this shard's projects env: PROJECTS: ${{ matrix.projects }} - BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }} + BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }} run: | set -euo pipefail touch "$RUNNER_TEMP/build-stamp" @@ -631,9 +665,10 @@ jobs: | tr '\n' ' ') modules="$modules $project_modules" done - # Always rebuild this job's changed files after every cache/artifact - # restore. A same-policy cache need not have timed them while changed. - # `check` requires fresh timings; `watch` retains the 60-minute limit. + # After every cache/artifact restore, `prepare` forces a rebuild of + # each changed file whose restored output has no recorded build time, + # so `check` judges a time measured in CI for every changed file. + # `watch` retains the 60-minute limit. time_base="" if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \ && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then @@ -817,15 +852,16 @@ jobs: - name: Build project id: compilation env: - BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }} + BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }} # This run's shards already compiled and timed these projects' # changed files, so assembly neither rebuilds nor re-times them. SHARD_PROJECTS: ${{ join(fromJSON(needs.plan.outputs.matrix).include.*.projects, ' ') }} run: | set -euo pipefail - # Always rebuild this job's changed files after every cache/artifact - # restore. A same-policy cache need not have timed them while changed. - # `check` requires fresh timings; `watch` retains the 60-minute limit. + # After every cache/artifact restore, `prepare` forces a rebuild of + # each changed file whose restored output has no recorded build time, + # so `check` judges a time measured in CI for every changed file. + # `watch` retains the 60-minute limit. time_base="" if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \ && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then @@ -1092,12 +1128,13 @@ jobs: - name: Build combined Lean root env: - BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }} + BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }} run: | set -euo pipefail - # Always rebuild this job's changed files after every cache/artifact - # restore. A same-policy cache need not have timed them while changed. - # `check` requires fresh timings; `watch` retains the 60-minute limit. + # After every cache/artifact restore, `prepare` forces a rebuild of + # each changed file whose restored output has no recorded build time, + # so `check` judges a time measured in CI for every changed file. + # `watch` retains the 60-minute limit. time_base="" if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \ && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then diff --git a/python/ci-performance.md b/python/ci-performance.md index 2d0b8455af..0f49dfb9c0 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -37,6 +37,25 @@ checkout, never the artifact paths. So every CI build step is followed by artifact lists, and preserves modification times, so shard packaging still ships only fresh files. +### Incremental PR pushes + +Until November 2026 every run recompiled every file a PR changed relative to +main, to time it against the 600 s limit. A PR that adds a 1,300-file project +therefore recompiled all of it (about 38 minutes on a 4-vCPU runner) on each +push, in the merge queue, and again on main, even when a push edited a handful +of files. + +Now `build_time_limits check` writes a `.timing.json` receipt beside each +changed module's output, bound to a hash of its `.olean` files, and `prepare` +only invalidates changed modules without a matching receipt. Receipts travel +with every artifact that carries the outputs themselves. `ci_pr_build` restores +the unchanged-source modules of the PR's newest successful run, so a later push +compiles only what it edited and whatever Lake's traces say depends on it. + +The plan and the build-time gate also measure a PR's changes from the tested +merge commit's first parent. The event's `base.sha` can trail main by days, +which made every project merged since look changed and be rebuilt. + 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/build_time_limits.py b/python/lean_pool/build_time_limits.py index 26f964ec44..ab1fe5b0f9 100644 --- a/python/lean_pool/build_time_limits.py +++ b/python/lean_pool/build_time_limits.py @@ -8,13 +8,21 @@ took longer than the per-file limit (600 seconds) to build. Existing files are only checked once a PR changes them. Times are the wall-clock -times Lake reports for each module on the CI runner. Standard library only, so CI -can run it with the runner's ``python3`` before ``uv`` is installed. +times Lake reports for each module on the CI runner. + +``check`` records each changed module's time in a receipt beside its compiled +output, bound to the hash of that output. ``prepare`` forces a rebuild of every +changed module whose output carries no matching receipt, so a file compiled +without being timed can never pass; a later run that restores the same output +reuses the recorded time instead of compiling the file again. Standard library +only, so CI can run it with the runner's ``python3`` before ``uv`` is installed. """ from __future__ import annotations import argparse +import hashlib +import json import logging import os import re @@ -32,6 +40,10 @@ FILE_LIMIT_SECONDS = 600 POLL_SECONDS = 15 TERMINATE_GRACE_SECONDS = 30 +RECEIPT_VERSION = 1 +RECEIPT_SUFFIX = ".timing.json" +# Every compiled output Lean loads for a module; a rebuild rewrites them all. +TIMED_OUTPUT_SUFFIXES = (".olean", ".olean.private", ".olean.server") _BUILT_LINE = re.compile( r"Built (?PLeanPool(?:\.[^\s:()]+)+) " r"\((?P\d+(?:\.\d+)?)(?Pms|s)\)" @@ -506,34 +518,116 @@ def _selected_changed_modules( } +def _output_stem(root: Path, path: str) -> Path: + """``LeanPool/A/B.lean`` -> ``/.lake/build/lib/lean/LeanPool/A/B``.""" + return root / ".lake/build/lib/lean" / Path(path).with_suffix("") + + +def output_digest(root: Path, path: str) -> str | None: + """Hash a module's compiled outputs; ``None`` when it has not been compiled.""" + stem = _output_stem(root, path) + digest = hashlib.sha256() + for suffix in TIMED_OUTPUT_SUFFIXES: + output = stem.with_name(stem.name + suffix) + try: + content = output.read_bytes() + except OSError: + if suffix == ".olean": + return None + continue + digest.update(f"{suffix}:{len(content)}:".encode()) + digest.update(content) + return digest.hexdigest() + + +def recorded_seconds(root: Path, path: str) -> float | None: + """The build time recorded for the module's current outputs, if any.""" + stem = _output_stem(root, path) + try: + receipt = json.loads(stem.with_name(stem.name + RECEIPT_SUFFIX).read_text()) + seconds = receipt["seconds"] + valid = ( + receipt["version"] == RECEIPT_VERSION + and isinstance(seconds, int | float) + and not isinstance(seconds, bool) + and seconds >= 0 + and receipt["outputs"] == output_digest(root, path) + ) + except (OSError, ValueError, KeyError, TypeError): + return None + return float(seconds) if valid else None + + +def record_seconds(root: Path, path: str, seconds: float) -> None: + """Bind a freshly measured build time to the outputs that build produced.""" + digest = output_digest(root, path) + if digest is None: + return + stem = _output_stem(root, path) + receipt = {"version": RECEIPT_VERSION, "seconds": seconds, "outputs": digest} + temporary = stem.with_name(stem.name + RECEIPT_SUFFIX + ".tmp") + temporary.write_text(json.dumps(receipt, sort_keys=True) + "\n") + temporary.replace(stem.with_name(stem.name + RECEIPT_SUFFIX)) + + +def _invalidate(root: Path, path: str) -> int: + """Remove every artifact of one module, including its timing receipt.""" + stem = Path(path).with_suffix("") + removed = 0 + for directory in ("lib/lean", "ir"): + target = root / ".lake/build" / directory / stem + if not target.parent.is_dir(): + continue + for artifact in target.parent.iterdir(): + if artifact.name.startswith(target.name + ".") and ( + artifact.is_file() or artifact.is_symlink() + ): + artifact.unlink() + removed += 1 + return removed + + def prepare( base: str, root: Path, modules: list[str] | None = None, exclude_projects: list[str] | None = None, ) -> int: - """Invalidate changed-module artifacts so their build must record new timings.""" + """Invalidate changed modules whose compiled outputs have no recorded time.""" changed = _selected_changed_modules(base, root, modules, exclude_projects) - removed = 0 - for path in changed.values(): - stem = Path(path).with_suffix("") - for directory in ("lib/lean", "ir"): - target = root / ".lake/build" / directory / stem - if not target.parent.is_dir(): - continue - for artifact in target.parent.iterdir(): - if artifact.name.startswith(target.name + ".") and ( - artifact.is_file() or artifact.is_symlink() - ): - artifact.unlink() - removed += 1 + untimed = [ + path for path in changed.values() if recorded_seconds(root, path) is None + ] + removed = sum(_invalidate(root, path) for path in untimed) print( - f"Fresh build timings: invalidated {removed} artifacts for " - f"{len(changed)} added or modified pool files." + f"Build timings: {len(changed)} added or modified pool files, " + f"{len(changed) - len(untimed)} with a recorded time for their compiled " + f"output; invalidated {removed} artifacts of the other {len(untimed)}." ) return 0 +def changed_times( + times: dict[str, float], changed: dict[str, str], root: Path +) -> tuple[dict[str, float], int]: + """Each changed module's time: measured in this job, else recorded earlier. + + Returns the times and how many came from this job's build. + """ + result = {} + fresh = 0 + for module, path in changed.items(): + if module in times: + record_seconds(root, path, times[module]) + result[module] = times[module] + fresh += 1 + continue + seconds = recorded_seconds(root, path) + if seconds is not None: + result[module] = seconds + return result, fresh + + def check( log_path: Path, base: str, @@ -544,21 +638,23 @@ def check( exclude_projects: list[str] | None = None, ) -> int: """Report changed files over the per-file limit; return the exit status.""" - times = module_times(log_path.read_text(errors="replace")) + built = module_times(log_path.read_text(errors="replace")) changed = _selected_changed_modules(base, root, modules, exclude_projects) - built = [module for module in changed if module in times] + times, fresh = changed_times(built, changed, root) print( f"Per-file build-time limit {limit} s: {len(changed)} added or modified " - f"pool files, {len(built)} compiled in this job." + f"pool files, {fresh} compiled in this job, {len(times) - fresh} with a " + "time recorded when their current output was compiled." ) - for module in sorted(built, key=lambda name: -times[name])[:10]: + for module in sorted(times, key=lambda name: -times[name])[:10]: print(f" {times[module]:8.1f} s {changed[module]}") found = violations(times, changed, limit) missing = sorted(set(changed) - times.keys()) for module in missing: print( - f"::error file={changed[module]}::No fresh successful build timing for " - f"{changed[module]}; added or modified files must compile in this job." + f"::error file={changed[module]}::No successful build timing for " + f"{changed[module]}; added or modified files must be compiled and " + "timed in CI." ) for violation in found: print( @@ -578,7 +674,7 @@ def main(arguments: list[str] | None = None) -> int: watch_parser.add_argument("--limit", type=int, default=PROCESS_LIMIT_SECONDS) watch_parser.add_argument("build", nargs=argparse.REMAINDER) prepare_parser = commands.add_parser( - "prepare", help="force changed files to rebuild" + "prepare", help="force untimed changed files to rebuild" ) prepare_parser.add_argument("--base", required=True) prepare_parser.add_argument("--root", type=Path, default=Path.cwd()) diff --git a/python/lean_pool/ci_pr_build.py b/python/lean_pool/ci_pr_build.py index c6894ebf80..27703822f4 100644 --- a/python/lean_pool/ci_pr_build.py +++ b/python/lean_pool/ci_pr_build.py @@ -88,6 +88,18 @@ def sources_match(root: Path, previous: str, base: str) -> bool: ) +def inputs_match(root: Path, previous: str) -> bool: + """Avoid downloading artifacts compiled under other pinned build inputs.""" + return ( + subprocess.run( + ["git", "diff", "--quiet", previous, "--", *rebase_fastpath.PINNED_INPUTS], + cwd=root, + check=False, + ).returncode + == 0 + ) + + def restore_prior_build( root: Path, repository: str, @@ -97,7 +109,12 @@ def restore_prior_build( base: str, current_run: int = 0, ) -> bool: - """Restore matching compiled files; Lake and every normal check still run.""" + """Restore the newest earlier build of this PR; Lake and every check still run. + + The PR's sources may have changed since that build. Only modules whose own + source is unchanged are restored; Lake recompiles the rest and any restored + module whose imports changed, and the build-time gate times what it compiles. + """ if not all(rebase_fastpath.SHA.fullmatch(value) for value in (head, base)): raise ValueError("invalid PR revisions") candidates = ( @@ -114,17 +131,19 @@ def restore_prior_build( except RECOVERY_ERRORS: LOGGER.info("Merged project reuse unavailable; checking the PR's build") for run in chain(() if history is None else (history,), candidates): - if not sources_match(root, run["head_sha"], base): + if not inputs_match(root, run["head_sha"]): continue try: - rebase_fastpath.restore(root, repository, run["id"], run["head_sha"]) - LOGGER.info("Restored matching PR build from run %s", run["id"]) + rebase_fastpath.restore( + root, repository, run["id"], run["head_sha"], changed_sources=True + ) + LOGGER.info("Restored unchanged modules from PR run %s", run["id"]) return True except RECOVERY_ERRORS: LOGGER.info( "PR build %s unavailable or changed; trying older run", run["id"] ) - LOGGER.info("No matching PR build; Lake will compile the current sources") + LOGGER.info("No earlier PR build; Lake will compile the current sources") return False diff --git a/python/lean_pool/rebase_fastpath.py b/python/lean_pool/rebase_fastpath.py index 7a20f0e383..352ab28d1c 100644 --- a/python/lean_pool/rebase_fastpath.py +++ b/python/lean_pool/rebase_fastpath.py @@ -348,8 +348,46 @@ def _restore_build_files( os.replace(staging / entry.name, destination) -def restore(root: Path, repository: str, run_id: int, previous_head: str) -> None: - """Download a prior green run's project artifacts and validate before overlay.""" +def _member_source(relative: PurePosixPath) -> str: + """The Lean source whose compilation produced a packed build file.""" + skip = 3 if relative.parts[2] == "ir" else 4 + return "/".join((*relative.parts[skip:-1], relative.name.split(".")[0] + ".lean")) + + +def _unchanged_members( + root: Path, members: list[tarfile.TarInfo], sources: dict[str, str] +) -> list[tarfile.TarInfo]: + """Keep the outputs of modules whose own source is the one that was compiled.""" + current = {} + kept = [] + for entry in members: + source = _member_source(PurePosixPath(entry.name)) + if source not in current: + path = root / source + current[source] = ( + hashlib.sha256(path.read_bytes()).hexdigest() + if path.is_file() + else None + ) + if current[source] is not None and sources.get(source) == current[source]: + kept.append(entry) + return kept + + +def restore( + root: Path, + repository: str, + run_id: int, + previous_head: str, + *, + changed_sources: bool = False, +) -> None: + """Download a prior green run's project artifacts and validate before overlay. + + With ``changed_sources``, project sources may differ from the packed build: + only modules whose own source is unchanged are restored, and Lake's traces + still decide which of those are reusable after their imports changed. + """ endpoint = f"repos/{repository}/actions/runs/{run_id}/artifacts?per_page=100" artifacts = [ artifact @@ -390,10 +428,12 @@ def restore(root: Path, repository: str, run_id: int, previous_head: str) -> Non for project in projects ): raise ValueError("invalid project build manifest") + sources = manifest.get("sources") if ( manifest.get("version") != 1 or manifest.get("head") != previous_head - or manifest.get("sources") != _source_hashes(root, projects) + or not isinstance(sources, dict) + or (not changed_sources and sources != _source_hashes(root, projects)) or manifest.get("inputs") != { name: hashlib.sha256((root / name).read_bytes()).hexdigest() @@ -412,6 +452,8 @@ def restore(root: Path, repository: str, run_id: int, previous_head: str) -> Non or not _build_file_for_project(relative, set(projects)) ): raise ValueError(f"unexpected project artifact: {entry.name}") + if changed_sources: + members = _unchanged_members(root, members, sources) _restore_build_files(root, archive, members) diff --git a/python/tests/test_build_time_limits.py b/python/tests/test_build_time_limits.py index 923272a452..73a32bf7b6 100644 --- a/python/tests/test_build_time_limits.py +++ b/python/tests/test_build_time_limits.py @@ -95,7 +95,7 @@ def test_violations_cover_changed_files_only( # At900s no observed module is too slow; Cached still lacks a fresh timing. assert limits.check(log, "base", tmp_path, limit=900) == 1 output = capsys.readouterr().out - assert "No fresh successful build timing for LeanPool/Quick/Cached.lean" in output + assert "No successful build timing for LeanPool/Quick/Cached.lean" in output def _git(root: Path, *arguments: str) -> str: @@ -254,9 +254,6 @@ def test_prepare_rebuilds_even_with_a_matching_legacy_policy_marker( """A global marker cannot certify a changed file on a later source reversion.""" root, base = _repository(tmp_path) changed = _outputs(root, BUNDLE_MODULE) - log = tmp_path / "build.log" - log.write_text(f"✔ [1/1] Built {BUNDLE_MODULE} (300s)\n") - assert limits.check(log, base, root, limit=600) == 0 marker = root / ".lake/build/lean-pool-build-time-policy" marker.write_text(hashlib.sha256(Path(limits.__file__).read_bytes()).hexdigest()) assert limits.prepare(base, root) == 0 @@ -576,7 +573,7 @@ def test_check_rejects_missing_or_replayed_changed_file_timing( log = tmp_path / "build.log" log.write_text(log_text) assert limits.check(log, base, root, 600) == 1 - assert "No fresh successful build timing" in capsys.readouterr().out + assert "No successful build timing" in capsys.readouterr().out def test_same_policy_source_revert_rebuilds_and_checks_slow_file(tmp_path: Path): @@ -603,6 +600,115 @@ def test_same_policy_source_revert_rebuilds_and_checks_slow_file(tmp_path: Path) assert limits.check(log, base, root, 600) == 0 +def _timed(root: Path, base: str, tmp_path: Path, seconds: int = 300) -> Path: + """Compile outputs for the changed bundle and record their build time.""" + artifact = _artifact(root, BUNDLE_MODULE, ".olean") + log = tmp_path / "timed.log" + log.write_text(f"Built {BUNDLE_MODULE} ({seconds}s)\n") + assert limits.check(log, base, root, 900) == 0 + return artifact + + +def test_recorded_time_spares_the_rebuild_of_unchanged_output(tmp_path: Path, capsys): + """Output timed by an earlier run is kept and passes without a fresh build.""" + root, base = _repository(tmp_path) + artifact = _timed(root, base, tmp_path) + assert limits.recorded_seconds(root, BUNDLE) == 300.0 + assert limits.prepare(base, root) == 0 + assert artifact.exists() + log = tmp_path / "build.log" + log.write_text(f"Replayed {BUNDLE_MODULE}\n") + capsys.readouterr() + assert limits.check(log, base, root, 600) == 0 + assert "0 compiled in this job, 1 with a time recorded" in capsys.readouterr().out + + +def test_recorded_time_over_the_limit_still_fails(tmp_path: Path, capsys): + """Reusing output never launders a slow file: its recorded time is checked.""" + root, base = _repository(tmp_path) + _timed(root, base, tmp_path, seconds=865) + log = tmp_path / "build.log" + log.write_text("") + assert limits.check(log, base, root, 600) == 1 + assert "took 865 s to build" in capsys.readouterr().out + + +@pytest.mark.parametrize("suffix", [".olean", ".olean.private", ".olean.server"]) +def test_recorded_time_does_not_cover_different_output(tmp_path: Path, suffix: str): + """A receipt certifies only the exact compiled files it was measured for.""" + root, base = _repository(tmp_path) + artifact = _timed(root, base, tmp_path) + _artifact(root, BUNDLE_MODULE, suffix).write_text("compiled by an untimed build\n") + assert limits.recorded_seconds(root, BUNDLE) is None + assert limits.prepare(base, root) == 0 + assert not artifact.exists() + stem = artifact.with_suffix("") + assert not stem.with_name(stem.name + limits.RECEIPT_SUFFIX).exists() + log = tmp_path / "build.log" + log.write_text("") + assert limits.check(log, base, root, 600) == 1 + + +@pytest.mark.parametrize( + "receipt", + [ + "{", + "[]", + '{"version": 0, "seconds": 1, "outputs": "DIGEST"}', + '{"version": 1, "seconds": true, "outputs": "DIGEST"}', + '{"version": 1, "seconds": -1, "outputs": "DIGEST"}', + '{"version": 1, "seconds": "1", "outputs": "DIGEST"}', + '{"version": 1, "outputs": "DIGEST"}', + '{"version": 1, "seconds": 1}', + ], +) +def test_malformed_receipts_certify_nothing(tmp_path: Path, receipt: str): + """Anything but a well-formed receipt for the current output forces a rebuild.""" + root, base = _repository(tmp_path) + artifact = _artifact(root, BUNDLE_MODULE, ".olean") + digest = limits.output_digest(root, BUNDLE) + stem = artifact.with_suffix("") + stem.with_name(stem.name + limits.RECEIPT_SUFFIX).write_text( + receipt.replace("DIGEST", digest) + ) + assert limits.recorded_seconds(root, BUNDLE) is None + assert limits.prepare(base, root) == 0 + assert not artifact.exists() + + +def test_fresh_build_replaces_the_recorded_time(tmp_path: Path): + """A module compiled in this job is judged by this job's measurement.""" + root, base = _repository(tmp_path) + _timed(root, base, tmp_path, seconds=865) + log = tmp_path / "build.log" + log.write_text(f"Built {BUNDLE_MODULE} (300s)\n") + assert limits.check(log, base, root, 600) == 0 + assert limits.recorded_seconds(root, BUNDLE) == 300.0 + + +def test_only_changed_modules_get_receipts(tmp_path: Path): + """Untouched files are outside the limit, so their builds record nothing.""" + root, base = _repository(tmp_path) + unchanged = "LeanPool/MovingSofa/Certificates/Bundle023.lean" + _artifact(root, BUNDLE_MODULE, ".olean") + _artifact(root, "LeanPool.MovingSofa.Certificates.Bundle023", ".olean") + log = tmp_path / "build.log" + log.write_text(LAKE_LOG.replace("(865s)", "(300s)")) + assert limits.check(log, base, root, 600) == 0 + assert limits.recorded_seconds(root, BUNDLE) == 300.0 + assert limits.recorded_seconds(root, unchanged) is None + + +def test_missing_output_records_nothing(tmp_path: Path): + """A timing without compiled output cannot certify a later restore.""" + root, base = _repository(tmp_path) + log = tmp_path / "build.log" + log.write_text(f"Built {BUNDLE_MODULE} (300s)\n") + assert limits.check(log, base, root, 600) == 0 + assert limits.recorded_seconds(root, BUNDLE) is None + assert limits.output_digest(root, BUNDLE) is None + + def test_prepare_and_check_scope_other_shard_and_explicit_empty(tmp_path: Path): """A shard checks only changed modules it builds; an empty scope checks none.""" root, base = _repository(tmp_path) @@ -749,8 +855,13 @@ def test_workflow_rebuilds_changed_modules_after_all_compiled_restores() -> None "build_time_limits check" ) assert script.count('--base "$time_base"') == 2 + assert steps[index]["env"]["BUILD_TIME_BASE"] == ( + "${{ needs.plan.outputs.diff_base }}" + ) assert 'git cat-file -e "$BUILD_TIME_BASE"' in script assert 'time_base=""' in script + if name != "rebase": + assert any("-m lean_pool.ci_pr_build" in s.get("run", "") for s in steps) if name == "shard": assert ( 'git ls-files -- "LeanPool/$project.lean" "LeanPool/$project/"' diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 0d3b53fe70..fc6bf67e50 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -267,11 +267,16 @@ def test_minimal_verifier_pr_has_an_explicit_project_build_producer(tmp_path): def test_assembly_restores_projects_once_and_main_owns_full_cache(): - """Assembly recovers PR outputs once before fresh shard files are applied.""" + """Shards and assembly recover PR outputs before fresh shard files are applied.""" jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + shard = [step.get("name") for step in jobs["shard"]["steps"]] + # A shard compiles only what a later push edited, so it needs the PR's + # earlier outputs (and their recorded build times) before it builds. + assert shard.index( + "Reuse compiled files from this PR's successful runs" + ) < shard.index("Build this shard's projects") assert not any( - "lean_pool.ci_pr_build" in step.get("run", "") - or "lean_pool.queue_build" in step.get("run", "") + "lean_pool.queue_build" in step.get("run", "") for step in jobs["shard"]["steps"] ) steps = jobs["finalize"]["steps"] diff --git a/python/tests/test_ci_pr_build.py b/python/tests/test_ci_pr_build.py index a833cd4bfe..e0abe6c92f 100644 --- a/python/tests/test_ci_pr_build.py +++ b/python/tests/test_ci_pr_build.py @@ -13,7 +13,13 @@ import pytest -from lean_pool import ci_artifacts, ci_pr_build, rebase_fastpath, slim_setup +from lean_pool import ( + build_time_limits, + ci_artifacts, + ci_pr_build, + rebase_fastpath, + slim_setup, +) TOOLCHAIN = (Path(__file__).resolve().parents[2] / "lean-toolchain").read_text().strip() @@ -175,19 +181,54 @@ def test_metadata_edit_reuses_build_without_skipping_validation( assert not (root / ".lake/validation-cache").exists() +@pytest.mark.parametrize( + ("path", "reused"), + [("LeanPool/B.lean", False), ("LeanPool/B/Added.lean", True)], +) +def test_changed_sources_restore_only_unchanged_modules( + repository, monkeypatch, path, reused +): + """An edited module is left for Lake to compile; untouched ones are restored.""" + root, base, previous = repository + archive, compiled = _archive(root, base, previous) + target = root / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text("module\n-- edited\n") + head = _commit(root, "edit source") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + assert compiled.exists() == reused + + +def test_deleted_module_output_is_not_restored(repository, monkeypatch): + """Compiled output of a module the PR has since removed stays out of the build.""" + root, base, previous = repository + (root / "LeanPool/B").mkdir() + (root / "LeanPool/B/Extra.lean").write_text("module\n") + previous = _commit(root, "add Extra") + extra = root / ".lake/build/lib/lean/LeanPool/B/Extra.olean" + extra.parent.mkdir(parents=True) + extra.write_text("prior compiled Extra") + archive, compiled = _archive(root, base, previous) + extra.unlink() + _git(root, "rm", "-q", "LeanPool/B/Extra.lean") + head = _commit(root, "remove Extra") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + assert compiled.exists() and not extra.exists() + + @pytest.mark.parametrize( "path", [ - "LeanPool/B.lean", - "LeanPool/B/Added.lean", "lean-toolchain", "lake-manifest.json", "lakefile.toml", "python/lean_pool/build_time_limits.py", ], ) -def test_changed_source_or_settings_avoid_download(repository, monkeypatch, path): - """Changed sources and build settings fall back before any artifact download.""" +def test_changed_settings_avoid_download(repository, monkeypatch, path): + """Changed build settings fall back before any artifact download.""" root, base, previous = repository archive, compiled = _archive(root, base, previous) target = root / path @@ -359,6 +400,63 @@ def test_lake_replays_and_rebuilds_after_setup_files_are_slimmed(repository): assert "rfl" in result.stdout + result.stderr +def _timed_build(lake: Path, root: Path, base: str) -> tuple[int, str]: + """Run the workflow's prepare, build and check sequence on both PR modules.""" + assert build_time_limits.prepare(base, root) == 0 + result = subprocess.run( + [str(lake), "build", "LeanPool.B", "LeanPool.C"], + cwd=root, + capture_output=True, + text=True, + ) + assert result.returncode == 0, result.stdout + result.stderr + log = root / "lean-build.log" + log.write_text(result.stdout + result.stderr) + return build_time_limits.check(log, base, root, 600), log.read_text() + + +def test_lake_recompiles_only_the_edited_module_of_an_earlier_pr_build( + repository, monkeypatch +): + """A later push compiles and times its edit; untouched modules keep their times.""" + root, base, _ = repository + lake = _lake() + (root / "LeanPool/C.lean").write_text("module\npublic def other : Nat := 3\n") + previous = _commit(root, "add C") + status, log = _timed_build(lake, root, base) + assert status == 0 and "Built LeanPool.B" in log and "Built LeanPool.C" in log + archive = root / "build.tar.gz" + rebase_fastpath.pack(root, base, previous, archive) + shutil.rmtree(root / ".lake/build") + (root / "LeanPool/C.lean").write_text("module\npublic def other : Nat := 4\n") + head = _commit(root, "edit C") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + status, log = _timed_build(lake, root, base) + assert status == 0 + assert "Built LeanPool.C" in log and "Built LeanPool.B" not in log + assert build_time_limits.recorded_seconds(root, "LeanPool/B.lean") is not None + + +def test_lake_output_restored_without_a_recorded_time_is_recompiled( + repository, monkeypatch +): + """Restored output that no CI run timed cannot satisfy the build-time gate.""" + root, base, previous = repository + lake = _lake() + subprocess.run( + [str(lake), "build", "LeanPool.B"], cwd=root, check=True, capture_output=True + ) + archive = root / "build.tar.gz" + rebase_fastpath.pack(root, base, previous, archive) + shutil.rmtree(root / ".lake/build") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", previous, base) + assert (root / ".lake/build/lib/lean/LeanPool/B.olean").is_file() + assert build_time_limits.prepare(base, root) == 0 + assert not (root / ".lake/build/lib/lean/LeanPool/B.olean").exists() + + def test_lake_keeps_unchanged_proof_after_metadata_edit(repository, monkeypatch): """Lake accepts matching artifacts without recompiling unchanged proofs.""" root, base, previous = repository @@ -382,18 +480,17 @@ def test_lake_keeps_unchanged_proof_after_metadata_edit(repository, monkeypatch) assert compiled.stat().st_mtime_ns == before -def test_untracked_source_inventory_rejected_before_overlay(repository, monkeypatch): - """The archive's full inventory also rejects an untracked added source.""" +def test_untracked_added_source_gets_no_restored_output(repository, monkeypatch): + """An added source has no earlier output; its unchanged neighbours are reused.""" root, base, previous = repository archive, compiled = _archive(root, base, previous) added = root / "LeanPool/B/Added.lean" added.parent.mkdir() added.write_text("module\n") _download(monkeypatch, archive, previous) - assert not ci_pr_build.restore_prior_build( - root, "owner/repo", 42, "pr", previous, base - ) - assert not compiled.exists() + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", previous, base) + assert compiled.read_text() == "prior compiled B" + assert not list((root / ".lake/build").rglob("Added.*")) def test_broken_archive_preserves_existing_build(repository, monkeypatch): From 1d6124bb9cdd8541bf8219d7c9681f7ccb07f2ac Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 14 Nov 2026 15:02:57 -0800 Subject: [PATCH 5/7] Lint and audit projects in the build shards, and shard when checkers change A change to any checker input invalidates every validation receipt. One job then linted the whole pool (~36 min) and audited it (~68 min), one project at a time, on the PR, in the merge queue, and again on main. - validation_cache: `shard --units ...` runs the per-project lint and quality checks for a shard's own projects and saves only its passes; `merge` adds shard passes to the assembling job's receipts. - Workflow: each shard validates the projects it built and uploads its passes; `finalize` merges them before the unchanged Lint and quality steps, which recompute every fingerprint and run whatever has no pass. - Planner: shard the whole pool when checker inputs change, even with a warm build cache; raise MAX_SHARDS from 10 to 14. Co-Authored-By: Claude Fable 5.2 --- .github/workflows/lean_action_ci.yml | 54 ++++++++- python/ci-performance.md | 20 ++++ python/lean_pool/validation_cache.py | 137 +++++++++++++++++++---- python/tests/test_build_shard_planner.py | 27 +++++ python/tests/test_ci_cache_contract.py | 30 +++++ python/tests/test_validation_cache.py | 99 ++++++++++++++++ scripts/ci/plan-build-shards.py | 37 +++++- 7 files changed, 381 insertions(+), 23 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index eeae274f49..a4788bfa82 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -629,7 +629,6 @@ jobs: fi - name: Install uv - if: github.event_name == 'pull_request' uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff with: enable-cache: true @@ -718,6 +717,44 @@ jobs: if-no-files-found: ignore retention-days: 1 + # Lint and audit this shard's projects here, in parallel with the other + # shards, instead of one after another in `finalize`. Only passes are + # handed on: `finalize` recomputes every fingerprint and runs whatever + # has no matching pass, so a failure here is reported there. + - name: Restore project validation + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/validation-cache/v1 + key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} + restore-keys: | + LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- + + - name: Install validation dependencies + continue-on-error: true + run: cd python && uv sync --locked + + - name: Lint and audit this shard's projects + id: shard-validation + continue-on-error: true + env: + PROJECTS: ${{ matrix.projects }} + run: | + cd python + # shellcheck disable=SC2086 # word-split the project list on purpose + uv run python -m lean_pool.validation_cache shard --repo .. --units $PROJECTS + + - name: Upload validation passes + if: always() && steps.shard-validation.outcome != 'skipped' + continue-on-error: true + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: ci-validation-${{ matrix.shard }} + path: .lake/validation-cache/v1/passes.json + include-hidden-files: true + if-no-files-found: ignore + compression-level: 1 + retention-days: 1 + finalize: needs: [plan, shard] # Run even when a shard failed: merging what succeeded and building the @@ -947,6 +984,21 @@ jobs: PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build --base "$BASE_SHA" --head "$HEAD_SHA" --receipts + - name: Download shard validation passes + continue-on-error: true + uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 + with: + pattern: ci-validation-* + path: ${{ runner.temp }}/shard-validation + + - name: Merge shard validation passes + continue-on-error: true + env: + FRAGMENTS: ${{ runner.temp }}/shard-validation + run: >- + PYTHONPATH=python python3 -m lean_pool.validation_cache merge + "$FRAGMENTS" + - name: Lint run: | cd python diff --git a/python/ci-performance.md b/python/ci-performance.md index 0f49dfb9c0..426d576491 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -56,6 +56,26 @@ The plan and the build-time gate also measure a PR's changes from the tested merge commit's first parent. The event's `base.sha` can trail main by days, which made every project merged since look changed and be rebuilt. +### Validation in shards + +Lint and the quality audits reuse per-project pass receipts, so an ordinary PR +validates only the project it touches. A change to any checker input (the +workflow, `validation_cache.py`, `quality.py`, the no-lint lists, the pins) +invalidates every receipt. One job then linted the pool for about 36 minutes and +audited it for about 68, one project at a time. + +In-job concurrency does not fix that: PR #785 measured that a single lint +process already saturates a 4-vCPU runner. Instead the planner now shards the +whole pool when checker inputs change, even with a warm build cache, and every +shard job lints and audits the projects it built +(`validation_cache shard --units ...`). Shards upload only their pass receipts. +`finalize` merges them (`validation_cache merge`) and then runs the unchanged +Lint and quality steps, which recompute every fingerprint, reuse matching passes, +and run anything a shard did not pass. A shard's validation step can therefore +neither fail nor pass the run by itself. + +`MAX_SHARDS` is 14: beyond that the costliest project fills a shard alone. + 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/validation_cache.py b/python/lean_pool/validation_cache.py index 4c6dfb9c7d..996eb7043d 100644 --- a/python/lean_pool/validation_cache.py +++ b/python/lean_pool/validation_cache.py @@ -3,6 +3,10 @@ CI restores receipts from main or earlier runs of the same PR. Every receipt covers module inventories, transitive local imports, dependency pins, and code. Static repository invariants and text style lint still run on every checkout. + +Build shards can validate their own projects in parallel (``shard``) and hand +their pass receipts to the assembling job (``merge``). That job still recomputes +every fingerprint and runs whatever a shard did not pass, so it alone decides. """ from __future__ import annotations @@ -47,6 +51,12 @@ def checker_inputs(kind: str | None) -> tuple[str, ...]: return GLOBAL_INPUTS +def unit_name(module: str) -> str: + """The pool unit that owns a module; the root index is its own unit.""" + parts = module.split(".") + return parts[1] if len(parts) > 1 else "__root__" + + def pool_units(root: Path) -> list[list[str]]: """Partition every pool source, including the root and unregistered modules.""" units: dict[str, list[str]] = {} @@ -115,14 +125,44 @@ def source_inventory( return paths +def read_receipts(path: Path) -> dict[str, dict[str, Any]]: + """Read a receipts file; a missing or corrupt one holds no receipts.""" + try: + data = json.loads(path.read_text()) + if data["version"] == 1 and isinstance(data["receipts"], dict): + return data["receipts"] + except (OSError, ValueError, KeyError, TypeError): + pass + return {} + + +def write_receipts(directory: Path, receipts: dict[str, dict[str, Any]]) -> None: + """Publish a receipts file atomically.""" + directory.mkdir(parents=True, exist_ok=True) + temporary = directory / "passes.tmp" + temporary.write_text(json.dumps({"version": 1, "receipts": receipts}) + "\n") + temporary.replace(directory / "passes.json") + + class ValidationCache: """Store pass receipts only, with content fingerprints and atomic publication.""" - def __init__(self, root: Path, directory: Path, *, refresh: bool = False) -> None: - """Load optional receipts; a missing or corrupt cache is a cold run.""" + def __init__( + self, + root: Path, + directory: Path, + *, + refresh: bool = False, + units: frozenset[str] | None = None, + ) -> None: + """Load optional receipts; a missing or corrupt cache is a cold run. + + With ``units``, checks of every other unit are skipped without a receipt. + """ self.root = root self.directory = directory self.refresh = refresh + self.units = units self.digests: dict[Path, str] = {} # Compilation finishes before validation; reuse inventories and path # lookups only within this immutable checkout, never across CI runs. @@ -135,12 +175,7 @@ def __init__(self, root: Path, directory: Path, *, refresh: bool = False) -> Non self.used: dict[str, dict[str, Any]] = {} self.hits = 0 self.misses = 0 - try: - data = json.loads((directory / "passes.json").read_text()) - if data["version"] == 1 and isinstance(data["receipts"], dict): - self.receipts = data["receipts"] - except (OSError, ValueError, KeyError, TypeError): - pass + self.receipts = read_receipts(directory / "passes.json") def fingerprint( self, modules: list[str], metadata: Any = None, *, kind: str | None = None @@ -188,6 +223,8 @@ def check[T]( metadata: Any = None, ) -> list[T]: """Run on a miss and retain only passes; failures never create receipts.""" + if self.units is not None and unit_name(modules[0]) not in self.units: + return [] digest = self.fingerprint(modules, metadata, kind=kind) key = f"{kind}:{modules[0]}" expected = {"fingerprint": digest, "modules": modules, "passed": True} @@ -205,21 +242,24 @@ def check[T]( def save(self) -> None: """Publish only receipts used in this run, pruning deleted/changed projects.""" - self.directory.mkdir(parents=True, exist_ok=True) - temporary = self.directory / "passes.tmp" - temporary.write_text(json.dumps({"version": 1, "receipts": self.used}) + "\n") - temporary.replace(self.directory / "passes.json") + write_receipts(self.directory, self.used) LOGGER.info( "Validation: %d cached checks, %d fresh checks", self.hits, self.misses ) -def lint_pool(root: Path, cache: ValidationCache) -> None: - """Lint owned declarations once per unit, importing every owned module.""" +def lint_pool( + root: Path, cache: ValidationCache, *, keep_going: bool = False +) -> list[str]: + """Lint owned declarations once per unit, importing every owned module. + + A failing unit raises, unless ``keep_going`` asks for its name instead. + """ + failed = [] for modules in pool_units(root): def validate() -> list[str]: - subprocess.run( + process = subprocess.run( [ "lake", "env", @@ -229,23 +269,82 @@ def validate() -> list[str]: *modules, ], cwd=root, - check=True, + check=not keep_going, ) - return [] + return [modules[0]] if process.returncode else [] - cache.check("lint", modules, validate) + failed.extend(cache.check("lint", modules, validate)) + return failed + + +def validate_shard(root: Path, cache: ValidationCache) -> bool: + """Lint and audit only the cache's units, keeping every pass they earn. + + This runs the per-project checks of the whole-pool run through the same + functions. Repository-wide invariants stay with the assembling job. + """ + from lean_pool.quality import _cached_pool_audits, _check_projects + + failed = lint_pool(root, cache, keep_going=True) + for unit in failed: + print(f"lint failed: {unit}") + errors = _check_projects(root, cache) + _cached_pool_audits(root, cache) + for error in errors: + print(error.format(root)) + cache.save() + return not (failed or errors) + + +def merge_receipts(directory: Path, fragments: list[Path]) -> int: + """Add shards' pass receipts to the cache; return how many were added. + + Each fragment is a receipts file or a directory of downloaded ones. + + A receipt only counts where the assembling job computes the same + fingerprint for the same modules, so merging cannot certify other inputs. + """ + receipts = read_receipts(directory / "passes.json") + added = 0 + files = [ + file + for fragment in fragments + for file in ( + sorted(fragment.rglob("passes.json")) if fragment.is_dir() else [fragment] + ) + ] + for fragment in files: + for key, receipt in read_receipts(fragment).items(): + if isinstance(receipt, dict) and receipts.get(key) != receipt: + receipts[key] = receipt + added += 1 + write_receipts(directory, receipts) + return added def main() -> int: """Run the cached declaration linter or repository quality checker.""" parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("check", choices=("lint", "quality")) + parser.add_argument("check", choices=("lint", "quality", "shard", "merge")) parser.add_argument("--repo", type=Path, default=Path.cwd()) parser.add_argument("--cache", type=Path, default=Path(".lake/validation-cache/v1")) parser.add_argument("--refresh", action="store_true") + parser.add_argument("--units", nargs="*", default=[]) + parser.add_argument("fragments", nargs="*", type=Path) arguments = parser.parse_args() logging.basicConfig(level=logging.INFO, format="validation: %(message)s") root = arguments.repo.resolve() + if arguments.check == "merge": + added = merge_receipts(root / arguments.cache, arguments.fragments) + LOGGER.info("Merged %d shard receipts", added) + return 0 + if arguments.check == "shard": + cache = ValidationCache( + root, + root / arguments.cache, + refresh=arguments.refresh, + units=frozenset(arguments.units), + ) + return 0 if validate_shard(root, cache) else 1 cache = ValidationCache(root, root / arguments.cache, refresh=arguments.refresh) if arguments.check == "lint": lint_pool(root, cache) diff --git a/python/tests/test_build_shard_planner.py b/python/tests/test_build_shard_planner.py index 3d4e26d0d3..2a28b2e836 100644 --- a/python/tests/test_build_shard_planner.py +++ b/python/tests/test_build_shard_planner.py @@ -177,6 +177,33 @@ def test_cold_plan_covers_pool_in_balanced_shards( assert max(loads) <= 1.25 * sum(loads) / len(loads) +def test_checker_input_change_fans_validation_out_over_the_pool( + monkeypatch: pytest.MonkeyPatch, + capsys: pytest.CaptureFixture[str], + tmp_path: Path, +) -> None: + """Every project must be validated again, so each shard takes its share.""" + listing = str(tmp_path / "changed.txt") + for changed in (".github/workflows/lean_action_ci.yml", "scripts/nolints.json"): + plan = _plan(monkeypatch, capsys, [changed], CHANGED_FILES_PATH=listing) + shards = plan["matrix"]["include"] + assert plan["mode"] == "sharded" + assert "lint or quality checker inputs changed" in plan["reason"] + projects = [name for shard in shards for name in shard["projects"].split()] + assert sorted(projects) == sorted(PLANNER["unit_sources"]()) + plan = _plan( + monkeypatch, capsys, ["python/lean_pool/stats.py"], CHANGED_FILES_PATH=listing + ) + assert plan["mode"] == "single" + + +def test_validation_inputs_match_the_receipt_fingerprints() -> None: + """The planner reads the checker inputs from the validation cache itself.""" + from lean_pool.validation_cache import GLOBAL_INPUTS + + assert PLANNER["validation_inputs"]() == set(GLOBAL_INPUTS) + + def test_dirty_projects_are_sharded_by_cost_only_when_large( monkeypatch: pytest.MonkeyPatch, capsys: pytest.CaptureFixture[str], diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index fc6bf67e50..0a6f37f24c 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -106,6 +106,36 @@ def test_single_and_sharded_builds_use_validation_cache() -> None: assert contracts[0] == contracts[1] +def test_shards_validate_their_projects_and_assembly_decides() -> None: + """Shard validation only hands passes on; it can never fail or pass the run.""" + jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + steps = jobs["shard"]["steps"] + names = [step.get("name") for step in steps] + validate = steps[names.index("Lint and audit this shard's projects")] + assert "validation_cache shard --repo .. --units $PROJECTS" in validate["run"] + assert validate["continue-on-error"] is True + assert names.index("Upload build outputs") < names.index( + "Lint and audit this shard's projects" + ) + upload = steps[names.index("Upload validation passes")] + assert upload["with"]["name"] == "ci-validation-${{ matrix.shard }}" + assert upload["continue-on-error"] is True + assert not any( + step.get("uses", "").startswith("actions/cache/save@") for step in steps + ) + final = jobs["finalize"]["steps"] + final_names = [step.get("name") for step in final] + merge = final[final_names.index("Merge shard validation passes")] + assert "validation_cache merge" in merge["run"] + assert ( + final_names.index("Restore project validation") + < final_names.index("Download shard validation passes") + < final_names.index("Merge shard validation passes") + < final_names.index("Lint") + < final_names.index("Repository quality checks") + ) + + def test_merge_queue_reports_all_required_gates_without_path_filtered_workflows() -> ( None ): diff --git a/python/tests/test_validation_cache.py b/python/tests/test_validation_cache.py index aa0f4df530..90b8851b31 100644 --- a/python/tests/test_validation_cache.py +++ b/python/tests/test_validation_cache.py @@ -13,8 +13,13 @@ GLOBAL_INPUTS, ValidationCache, _module_sources, + lint_pool, + merge_receipts, pool_units, + read_receipts, source_inventory, + unit_name, + validate_shard, ) @@ -292,3 +297,97 @@ def test_inventory_fallback_preserves_discovered_external_dependencies( assert cache.check(kind, modules, lambda: ["changed dependency"]) == [ "changed dependency" ] + + +def _shard(root: Path, *units: str) -> ValidationCache: + return ValidationCache( + root, root / ".lake/validation-cache/v1", units=frozenset(units) + ) + + +def test_units_belong_to_their_project_and_the_root_to_itself() -> None: + """Shard project names select the same units the pool is partitioned into.""" + assert unit_name("LeanPool.A.Detail") == unit_name("LeanPool.A") == "A" + assert unit_name("LeanPool") == "__root__" + + +def test_shard_cache_validates_only_its_units(repository: Path) -> None: + """Other shards' units are neither run nor given a receipt.""" + cache = _shard(repository, "A") + calls: list[str] = [] + for modules in pool_units(repository): + cache.check("lint", modules, lambda: calls.append(modules[0]) or []) + assert calls == ["LeanPool.A"] + assert list(cache.used) == ["lint:LeanPool.A"] + + +def test_shard_passes_satisfy_the_whole_pool_run_only_while_inputs_match( + repository: Path, +) -> None: + """Merged passes are reused by fingerprint; an edited project is checked again.""" + with ( + patch("lean_pool.validation_cache.subprocess.run") as lint, + patch("lean_pool.quality._check_projects", return_value=[]), + patch("lean_pool.quality._audit_axioms", return_value=[]), + patch("lean_pool.quality._run_option_audit", return_value=[]), + ): + lint.return_value.returncode = 0 + fragment = repository / "fragments/ci-validation-00" + shard = ValidationCache(repository, fragment, units=frozenset({"A"})) + assert validate_shard(repository, shard) + assert sorted(read_receipts(fragment / "passes.json")) == [ + "axioms:LeanPool.A", + "backdoors:LeanPool.A", + "lint:LeanPool.A", + ] + directory = repository / ".lake/validation-cache/v1" + assert merge_receipts(directory, [fragment.parent]) == 3 + assert merge_receipts(directory, [fragment / "passes.json"]) == 0 + assert _run(repository)[1] == ["LeanPool.B", "LeanPool"] + (repository / "LeanPool/A.lean").write_text("-- edited after the shard ran\n") + merge_receipts(directory, [fragment.parent]) + assert _run(repository)[1] == ["LeanPool.A", "LeanPool"] + + +def test_shard_keeps_passes_and_reports_a_failing_unit(repository: Path) -> None: + """One failing project costs the assembling job only that project's checks.""" + + def lint(command, **kwargs): + assert kwargs["check"] is False + failed = "LeanPool.A" in command + return type("Process", (), {"returncode": int(failed)})() + + with ( + patch("lean_pool.validation_cache.subprocess.run", side_effect=lint), + patch("lean_pool.quality._check_projects", return_value=[]), + patch("lean_pool.quality._audit_axioms", return_value=[]), + patch("lean_pool.quality._run_option_audit", return_value=[]), + ): + shard = _shard(repository, "A", "B") + assert not validate_shard(repository, shard) + saved = read_receipts(repository / ".lake/validation-cache/v1/passes.json") + assert "lint:LeanPool.B" in saved and "lint:LeanPool.A" not in saved + assert "axioms:LeanPool.A" in saved + + +def test_whole_pool_lint_still_stops_at_a_failing_unit(repository: Path) -> None: + """Outside a shard the linter's failure remains a hard error.""" + cache = ValidationCache(repository, repository / ".lake/validation-cache/v1") + with patch("lean_pool.validation_cache.subprocess.run") as lint: + lint_pool(repository, cache) + assert all(call.kwargs["check"] is True for call in lint.call_args_list) + + +def test_corrupt_fragments_merge_nothing(repository: Path) -> None: + """Unreadable or malformed shard output leaves the cache as it was.""" + directory = repository / ".lake/validation-cache/v1" + _run(repository) + before = read_receipts(directory / "passes.json") + bad = repository / "fragments" + bad.mkdir() + (bad / "passes.json").write_text("{") + listed = bad / "list" + listed.mkdir() + (listed / "passes.json").write_text('{"version": 1, "receipts": {"lint:X": 1}}') + assert merge_receipts(directory, [bad, repository / "missing.json"]) == 0 + assert read_receipts(directory / "passes.json") == before diff --git a/scripts/ci/plan-build-shards.py b/scripts/ci/plan-build-shards.py index 55d22c511d..9514b8b0a0 100644 --- a/scripts/ci/plan-build-shards.py +++ b/scripts/ci/plan-build-shards.py @@ -12,7 +12,10 @@ classic one-job pipeline — the fast path for a typical PR that adds or edits one project. `sharded` splits the build across parallel jobs for the cases that take hours serially: a cold cache, a -toolchain/manifest bump, or a refactor touching many projects. +toolchain/manifest bump, a refactor touching many projects, or a change to +the lint and quality checkers' own inputs. That last case replays the build +from the warm cache, but every project must be linted and audited again +(about 100 minutes in one job), which each shard does for its own projects. Everything is computed at run time from the repository tree and the diff, so there is no static shard assignment to maintain as the pool grows. @@ -37,13 +40,17 @@ FORCE_FULL "true" to shard-build the whole pool regardless. """ +import ast import json import math import os import sys from pathlib import Path -MAX_SHARDS = 10 +# Shards also validate their projects, so a whole-pool run is bounded by its +# slowest shard. Beyond this the costliest project (MovingSofa, about 350 +# CPU-minutes cold) fills a shard alone and more shards stop helping. +MAX_SHARDS = 14 FILES_PER_SHARD = 250 # Below either threshold a serial build is already fast; sharding would # only add scheduling and artifact overhead to the common import PR. @@ -57,6 +64,25 @@ "scripts/ci/LeanPoolLinters.lean", } BUILD_COSTS_PATH = Path(__file__).with_name("build-costs.json") +VALIDATION_CACHE_PATH = ( + Path(__file__).resolve().parents[2] / "python/lean_pool/validation_cache.py" +) + + +def validation_inputs(path: Path = VALIDATION_CACHE_PATH) -> set[str]: + """Files whose change invalidates every project's lint and quality receipt. + + Read from the validation cache itself, without importing the package, so + this list cannot drift from the fingerprints it predicts. + """ + module = ast.parse(path.read_text()) + values: dict[str, tuple[str, ...]] = {} + for node in module.body: + if isinstance(node, ast.Assign) and isinstance(node.targets[0], ast.Name): + name = node.targets[0].id + if name in {"SHARED_INPUTS", "LINT_INPUTS", "QUALITY_INPUTS"}: + values[name] = tuple(ast.literal_eval(node.value)) + return {name for names in values.values() for name in names} def unit_sources() -> dict[str, list[Path]]: @@ -215,7 +241,10 @@ def main() -> None: sources = unit_sources() file_counts = {name: len(paths) for name, paths in sources.items()} global_change = bool(GLOBAL_BUILD_INPUTS.intersection(changed_files)) - full = cold or force_full or global_change or not diff_available + validation_change = bool(validation_inputs().intersection(changed_files)) + full = ( + cold or force_full or global_change or validation_change or not diff_available + ) if full: targets = set(file_counts) @@ -225,6 +254,8 @@ def main() -> None: reason = "no warm build cache" elif global_change: reason = "shared compiler or build inputs changed" + elif validation_change: + reason = "lint or quality checker inputs changed" else: reason = "no diff available for this event" else: From c2bd07d29ca96a9164d44c3084fc75a1b7df7b2a Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 14 Nov 2026 15:11:05 -0800 Subject: [PATCH 6/7] Move shard validation into its own module with top-level imports quality.py imports validation_cache.py, so the shard entry point could only reach the quality checks through a function-level import. A separate module imports both at the top. Its source joins the receipt fingerprints. Co-Authored-By: Claude Fable 5.2 --- .github/workflows/lean_action_ci.yml | 2 +- python/ci-performance.md | 2 +- python/lean_pool/shard_validation.py | 49 ++++++++++++++++++++++++++ python/lean_pool/validation_cache.py | 37 ++++--------------- python/tests/test_ci_cache_contract.py | 2 +- python/tests/test_validation_cache.py | 25 +++++++++++-- 6 files changed, 80 insertions(+), 37 deletions(-) create mode 100644 python/lean_pool/shard_validation.py diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index a4788bfa82..7096aa7d75 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -741,7 +741,7 @@ jobs: run: | cd python # shellcheck disable=SC2086 # word-split the project list on purpose - uv run python -m lean_pool.validation_cache shard --repo .. --units $PROJECTS + uv run python -m lean_pool.shard_validation --repo .. --units $PROJECTS - name: Upload validation passes if: always() && steps.shard-validation.outcome != 'skipped' diff --git a/python/ci-performance.md b/python/ci-performance.md index 426d576491..35aeb818e1 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -68,7 +68,7 @@ In-job concurrency does not fix that: PR #785 measured that a single lint process already saturates a 4-vCPU runner. Instead the planner now shards the whole pool when checker inputs change, even with a warm build cache, and every shard job lints and audits the projects it built -(`validation_cache shard --units ...`). Shards upload only their pass receipts. +(`python -m lean_pool.shard_validation --units ...`). Shards upload only their pass receipts. `finalize` merges them (`validation_cache merge`) and then runs the unchanged Lint and quality steps, which recompute every fingerprint, reuse matching passes, and run anything a shard did not pass. A shard's validation step can therefore diff --git a/python/lean_pool/shard_validation.py b/python/lean_pool/shard_validation.py new file mode 100644 index 0000000000..645c63a97f --- /dev/null +++ b/python/lean_pool/shard_validation.py @@ -0,0 +1,49 @@ +"""Lint and audit one build shard's projects, keeping every pass they earn. + +A shard job runs this for the projects it built, in parallel with the other +shards, and uploads the resulting pass receipts. It runs the per-project checks +of the whole-pool run through the same functions. Repository-wide invariants, +and the decision itself, stay with the assembling job: it merges the receipts +(``validation_cache merge``), recomputes every fingerprint, and runs whatever +has no matching pass. +""" + +from __future__ import annotations + +import argparse +import logging +from pathlib import Path + +from lean_pool.quality import _cached_pool_audits, _check_projects +from lean_pool.validation_cache import ValidationCache, lint_pool + +LOGGER = logging.getLogger(__name__) + + +def validate_shard(root: Path, cache: ValidationCache) -> bool: + """Lint and audit only the cache's units; save their passes either way.""" + failed = lint_pool(root, cache, keep_going=True) + for unit in failed: + print(f"lint failed: {unit}") + errors = _check_projects(root, cache) + _cached_pool_audits(root, cache) + for error in errors: + print(error.format(root)) + cache.save() + return not (failed or errors) + + +def main(arguments: list[str] | None = None) -> int: + """Validate the named units and report whether all of them passed.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=Path.cwd()) + parser.add_argument("--cache", type=Path, default=Path(".lake/validation-cache/v1")) + parser.add_argument("--units", nargs="*", default=[]) + options = parser.parse_args(arguments) + logging.basicConfig(level=logging.INFO, format="validation: %(message)s") + root = options.repo.resolve() + cache = ValidationCache(root, root / options.cache, units=frozenset(options.units)) + return 0 if validate_shard(root, cache) else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/python/lean_pool/validation_cache.py b/python/lean_pool/validation_cache.py index 996eb7043d..47a17acc12 100644 --- a/python/lean_pool/validation_cache.py +++ b/python/lean_pool/validation_cache.py @@ -4,9 +4,10 @@ covers module inventories, transitive local imports, dependency pins, and code. Static repository invariants and text style lint still run on every checkout. -Build shards can validate their own projects in parallel (``shard``) and hand -their pass receipts to the assembling job (``merge``). That job still recomputes -every fingerprint and runs whatever a shard did not pass, so it alone decides. +Build shards can validate their own projects in parallel +(``lean_pool.shard_validation``) and hand their pass receipts to the assembling +job (``merge``). That job still recomputes every fingerprint and runs whatever a +shard did not pass, so it alone decides. """ from __future__ import annotations @@ -28,6 +29,7 @@ "lakefile.lean", "scripts/ci/LeanPoolLinters.lean", "python/lean_pool/validation_cache.py", + "python/lean_pool/shard_validation.py", "python/pyproject.toml", "python/uv.lock", ".github/workflows/lean_action_ci.yml", @@ -277,24 +279,6 @@ def validate() -> list[str]: return failed -def validate_shard(root: Path, cache: ValidationCache) -> bool: - """Lint and audit only the cache's units, keeping every pass they earn. - - This runs the per-project checks of the whole-pool run through the same - functions. Repository-wide invariants stay with the assembling job. - """ - from lean_pool.quality import _cached_pool_audits, _check_projects - - failed = lint_pool(root, cache, keep_going=True) - for unit in failed: - print(f"lint failed: {unit}") - errors = _check_projects(root, cache) + _cached_pool_audits(root, cache) - for error in errors: - print(error.format(root)) - cache.save() - return not (failed or errors) - - def merge_receipts(directory: Path, fragments: list[Path]) -> int: """Add shards' pass receipts to the cache; return how many were added. @@ -324,11 +308,10 @@ def merge_receipts(directory: Path, fragments: list[Path]) -> int: def main() -> int: """Run the cached declaration linter or repository quality checker.""" parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("check", choices=("lint", "quality", "shard", "merge")) + parser.add_argument("check", choices=("lint", "quality", "merge")) parser.add_argument("--repo", type=Path, default=Path.cwd()) parser.add_argument("--cache", type=Path, default=Path(".lake/validation-cache/v1")) parser.add_argument("--refresh", action="store_true") - parser.add_argument("--units", nargs="*", default=[]) parser.add_argument("fragments", nargs="*", type=Path) arguments = parser.parse_args() logging.basicConfig(level=logging.INFO, format="validation: %(message)s") @@ -337,14 +320,6 @@ def main() -> int: added = merge_receipts(root / arguments.cache, arguments.fragments) LOGGER.info("Merged %d shard receipts", added) return 0 - if arguments.check == "shard": - cache = ValidationCache( - root, - root / arguments.cache, - refresh=arguments.refresh, - units=frozenset(arguments.units), - ) - return 0 if validate_shard(root, cache) else 1 cache = ValidationCache(root, root / arguments.cache, refresh=arguments.refresh) if arguments.check == "lint": lint_pool(root, cache) diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 0a6f37f24c..e96c0e3dc7 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -112,7 +112,7 @@ def test_shards_validate_their_projects_and_assembly_decides() -> None: steps = jobs["shard"]["steps"] names = [step.get("name") for step in steps] validate = steps[names.index("Lint and audit this shard's projects")] - assert "validation_cache shard --repo .. --units $PROJECTS" in validate["run"] + assert "lean_pool.shard_validation --repo .. --units $PROJECTS" in validate["run"] assert validate["continue-on-error"] is True assert names.index("Upload build outputs") < names.index( "Lint and audit this shard's projects" diff --git a/python/tests/test_validation_cache.py b/python/tests/test_validation_cache.py index 90b8851b31..a0d2719dee 100644 --- a/python/tests/test_validation_cache.py +++ b/python/tests/test_validation_cache.py @@ -9,6 +9,8 @@ import pytest from lean_pool.quality import _cached_pool_audits +from lean_pool.shard_validation import main as shard_main +from lean_pool.shard_validation import validate_shard from lean_pool.validation_cache import ( GLOBAL_INPUTS, ValidationCache, @@ -19,7 +21,6 @@ read_receipts, source_inventory, unit_name, - validate_shard, ) @@ -327,7 +328,7 @@ def test_shard_passes_satisfy_the_whole_pool_run_only_while_inputs_match( """Merged passes are reused by fingerprint; an edited project is checked again.""" with ( patch("lean_pool.validation_cache.subprocess.run") as lint, - patch("lean_pool.quality._check_projects", return_value=[]), + patch("lean_pool.shard_validation._check_projects", return_value=[]), patch("lean_pool.quality._audit_axioms", return_value=[]), patch("lean_pool.quality._run_option_audit", return_value=[]), ): @@ -359,7 +360,7 @@ def lint(command, **kwargs): with ( patch("lean_pool.validation_cache.subprocess.run", side_effect=lint), - patch("lean_pool.quality._check_projects", return_value=[]), + patch("lean_pool.shard_validation._check_projects", return_value=[]), patch("lean_pool.quality._audit_axioms", return_value=[]), patch("lean_pool.quality._run_option_audit", return_value=[]), ): @@ -391,3 +392,21 @@ def test_corrupt_fragments_merge_nothing(repository: Path) -> None: (listed / "passes.json").write_text('{"version": 1, "receipts": {"lint:X": 1}}') assert merge_receipts(directory, [bad, repository / "missing.json"]) == 0 assert read_receipts(directory / "passes.json") == before + + +def test_shard_command_validates_the_named_units(repository: Path) -> None: + """The workflow's entry point scopes the cache to its project list.""" + with ( + patch("lean_pool.validation_cache.subprocess.run") as lint, + patch("lean_pool.shard_validation._check_projects", return_value=[]), + patch("lean_pool.quality._audit_axioms", return_value=[]), + patch("lean_pool.quality._run_option_audit", return_value=[]), + ): + lint.return_value.returncode = 0 + assert shard_main(["--repo", str(repository), "--units", "B"]) == 0 + saved = read_receipts(repository / ".lake/validation-cache/v1/passes.json") + assert sorted(saved) == [ + "axioms:LeanPool.B", + "backdoors:LeanPool.B", + "lint:LeanPool.B", + ] From 64b3fad333f4171ea0b4a6dc994bfb46eafaa34c Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 14 Nov 2026 15:18:32 -0800 Subject: [PATCH 7/7] Move a test import to the top of the file Co-Authored-By: Claude Fable 5.2 --- python/tests/test_build_shard_planner.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/python/tests/test_build_shard_planner.py b/python/tests/test_build_shard_planner.py index 2a28b2e836..d770d166ec 100644 --- a/python/tests/test_build_shard_planner.py +++ b/python/tests/test_build_shard_planner.py @@ -8,6 +8,8 @@ import pytest +from lean_pool.validation_cache import GLOBAL_INPUTS + ROOT = Path(__file__).resolve().parents[2] PLANNER = runpy.run_path(str(ROOT / "scripts/ci/plan-build-shards.py")) MEASURER = runpy.run_path(str(ROOT / "scripts/ci/measure-build-costs.py")) @@ -199,8 +201,6 @@ def test_checker_input_change_fans_validation_out_over_the_pool( def test_validation_inputs_match_the_receipt_fingerprints() -> None: """The planner reads the checker inputs from the validation cache itself.""" - from lean_pool.validation_cache import GLOBAL_INPUTS - assert PLANNER["validation_inputs"]() == set(GLOBAL_INPUTS)