diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 62c752b08f..1c82f0de20 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -317,12 +317,20 @@ jobs: exit 1 fi - # Publish once compilation succeeds, so docs can overlap the later - # linters/quality checks. Rare PRs requiring the minimal-file gate share - # this exact-tree output too, avoiding a second cold whole-pool build. + # Main publishes the shared full build. A minimal-verifier PR publishes + # only its own projects; the verifier overlays them on the main cache. - name: Package build for documentation if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') - run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack + env: + BUILD_EVENT: ${{ github.event_name }} + BASE_SHA: ${{ github.event.pull_request.base.sha }} + HEAD_SHA: ${{ github.event.pull_request.head.sha }} + run: | + if [ "$BUILD_EVENT" = pull_request ]; then + PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack --base "$BASE_SHA" --head "$HEAD_SHA" + else + PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack + fi - name: Share build with documentation if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') @@ -632,6 +640,22 @@ jobs: echo "Mathlib already present from cache" fi + # Recover PR outputs once; fresh shard files are layered on afterwards. + - 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: Download shard build outputs uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 with: @@ -679,12 +703,20 @@ jobs: exit 1 fi - # Publish once compilation succeeds, so docs can overlap the later - # linters/quality checks. Rare PRs requiring the minimal-file gate share - # this exact-tree output too, avoiding a second cold whole-pool build. + # Main publishes the shared full build. A minimal-verifier PR publishes + # only its own projects; the verifier overlays them on the main cache. - name: Package build for documentation if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') - run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack + env: + BUILD_EVENT: ${{ github.event_name }} + BASE_SHA: ${{ github.event.pull_request.base.sha }} + HEAD_SHA: ${{ github.event.pull_request.head.sha }} + run: | + if [ "$BUILD_EVENT" = pull_request ]; then + PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack --base "$BASE_SHA" --head "$HEAD_SHA" + else + PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack + fi - name: Share build with documentation if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') diff --git a/python/lean_pool/ci_artifacts.py b/python/lean_pool/ci_artifacts.py index 903239e556..f4c2e884d7 100644 --- a/python/lean_pool/ci_artifacts.py +++ b/python/lean_pool/ci_artifacts.py @@ -1,9 +1,11 @@ -"""Share the current Lean CI build with documentation without sharing mutable caches. +"""Share main's full build and PR project overlays with independent consumers. Only the matching Lean Action CI run is queried. A source-tree/configuration manifest is verified before any artifact is installed; Lake still checks its normal build traces afterwards. Missing or incompatible artifacts fall back to -the ordinary documentation build. +the ordinary Lake build. PR overlays preserve the shared main cache and contain +only projects changed in the author's diff, including a manifest-only archive +for infrastructure changes. """ from __future__ import annotations @@ -16,6 +18,7 @@ import json import logging import os +import re import shutil import stat import subprocess @@ -34,6 +37,43 @@ ARCHIVE_NAME = "lean-pool-build.tar.zst" LEGACY_ARCHIVE_NAME = "lean-pool-build.tar.gz" MANIFEST_NAME = "build-manifest.json" +PROJECT = re.compile(r"[A-Za-z][A-Za-z0-9_]*\Z") + + +def _project_output(path: PurePosixPath, projects: list[str]) -> bool: + """Restrict overlays to the changed projects' Lean library and IR files.""" + for prefix in ( + (".lake", "build", "ir", "LeanPool"), + (".lake", "build", "lib", "lean", "LeanPool"), + ): + if path.parts[: len(prefix)] == prefix and len(path.parts) > len(prefix): + module = path.parts[len(prefix)] + return any( + module == name or module.startswith(name + ".") for name in projects + ) + return False + + +def _changed_projects(root: Path, base: str, head: str) -> list[str]: + """Select PR-owned projects from the author diff, excluding changes on main.""" + paths = ( + subprocess.check_output( + ["git", "diff", "--name-only", "-z", f"{base}...{head}", "--", "LeanPool"], + cwd=root, + ) + .decode() + .split("\0") + ) + projects = sorted( + { + path.split("/")[1].removesuffix(".lean") + for path in paths + if path.startswith("LeanPool/") and path.endswith(".lean") + } + ) + if not all(PROJECT.fullmatch(name) for name in projects): + raise ValueError("invalid changed project") + return projects def _file_digest(path: Path) -> str: @@ -93,16 +133,31 @@ def _compressed_stream(path: Path, *, writing: bool = False): process.wait() -def pack_build(root: Path, destination: Path) -> None: - """Package all completed build files using fast, bounded-memory compression.""" +def pack_build( + root: Path, destination: Path, *, base: str = "", head: str = "" +) -> None: + """Package main's full build or only PR-owned projects for a verifier overlay.""" subprocess.run(["git", "diff", "--exit-code", "HEAD", "--"], cwd=root, check=True) - payload = json.dumps(build_identity(root)).encode() + identity = build_identity(root) + if bool(base) != bool(head): + raise ValueError("project packaging requires both base and head") + if base: + identity["projects"] = _changed_projects(root, base, head) + payload = json.dumps(identity).encode() manifest = tarfile.TarInfo(MANIFEST_NAME) manifest.size = len(payload) with _compressed_stream(destination, writing=True) as stream: with tarfile.open(fileobj=stream, mode="w|", dereference=True) as archive: archive.addfile(manifest, io.BytesIO(payload)) - archive.add(root / ".lake/build", arcname=".lake/build") + if "projects" not in identity: + archive.add(root / ".lake/build", arcname=".lake/build") + else: + for path in sorted((root / ".lake/build").rglob("*")): + relative = PurePosixPath(path.relative_to(root).as_posix()) + if path.is_file() and _project_output( + relative, identity["projects"] + ): + archive.add(path, arcname=str(relative), recursive=False) def _reuse_unchanged_file( @@ -131,14 +186,26 @@ def _extract_build( archive: tarfile.TarFile, temporary: Path, reused: dict[Path, os.stat_result], -) -> bool: +) -> str | None: """Check the manifest first, then extract only ordinary build files.""" manifest = archive.next() if manifest is None or manifest.name != MANIFEST_NAME or not manifest.isfile(): raise ValueError("Missing build archive manifest") - if json.load(archive.extractfile(manifest)) != build_identity(root): + identity = json.load(archive.extractfile(manifest)) + if not isinstance(identity, dict): + raise ValueError("invalid build archive manifest") + project_overlay = "projects" in identity + projects = identity.pop("projects", None) + if project_overlay and ( + not isinstance(projects, list) + or not all( + isinstance(name, str) and PROJECT.fullmatch(name) for name in projects + ) + ): + raise ValueError("invalid project overlay") + if identity != build_identity(root): LOGGER.info("CI build has different sources or configuration; rebuilding") - return False + return None has_files = False seen: set[PurePosixPath] = set() for member in archive: @@ -150,6 +217,10 @@ def _extract_build( or ".." in path.parts or path in seen or not (member.isfile() or member.isdir()) + or ( + projects is not None + and (not member.isfile() or not _project_output(path, projects)) + ) ): raise ValueError(f"Unexpected build archive member: {member.name}") seen.add(path) @@ -157,9 +228,9 @@ def _extract_build( archive.extract(member, temporary, filter="data") if member.isfile(): _reuse_unchanged_file(root, temporary, member, reused) - if not has_files: + if not has_files and projects is None: raise ValueError("Empty Lean build artifact") - return True + return "full" if projects is None else "projects" def restore_build(root: Path, archive_path: Path) -> bool: @@ -177,12 +248,20 @@ def _restore_archive(root: Path, payload: AbstractContextManager[BinaryIO]) -> b reused: dict[Path, os.stat_result] = {} with payload as stream: with tarfile.open(fileobj=stream, mode="r|") as archive: - if not _extract_build(root, archive, temporary, reused): + mode = _extract_build(root, archive, temporary, reused) + if not mode: return False destination = root / ".lake/build" - if destination.exists(): - shutil.rmtree(destination) - (temporary / ".lake/build").rename(destination) + if mode == "full": + if destination.exists(): + shutil.rmtree(destination) + (temporary / ".lake/build").rename(destination) + else: + for staged in (temporary / ".lake/build").rglob("*"): + if staged.is_file(): + target = root / staged.relative_to(temporary) + target.parent.mkdir(parents=True, exist_ok=True) + os.replace(staged, target) for relative, metadata in reused.items(): path = root / relative path.chmod(stat.S_IMODE(metadata.st_mode)) @@ -343,6 +422,8 @@ def main() -> None: commands = parser.add_subparsers(dest="command", required=True) pack = commands.add_parser("pack") pack.add_argument("--output", type=Path, default=Path(ARCHIVE_NAME)) + pack.add_argument("--base", default="") + pack.add_argument("--head", default="") restore = commands.add_parser("restore") waiting = commands.add_parser("wait") for command in (restore, waiting): @@ -356,7 +437,9 @@ def main() -> None: arguments = parser.parse_args() logging.basicConfig(level=logging.INFO, format="ci-artifacts: %(message)s") if arguments.command == "pack": - pack_build(Path.cwd(), arguments.output) + pack_build( + Path.cwd(), arguments.output, base=arguments.base, head=arguments.head + ) elif arguments.command == "wait": wait_for_build( arguments.repository, diff --git a/python/tests/test_ci_artifacts.py b/python/tests/test_ci_artifacts.py index 0eccce24d7..12ef5ec035 100644 --- a/python/tests/test_ci_artifacts.py +++ b/python/tests/test_ci_artifacts.py @@ -467,3 +467,93 @@ def matching(repository_name, head, event): ) assert calls == [("owner/repo", "head", "pull_request")] assert output.exists() + + +@pytest.mark.parametrize("content_change", [False, True]) +def test_project_archive_preserves_shared_main_build(repository, content_change): + """Infrastructure emits a manifest only; content overlays its own project.""" + base = subprocess.check_output( + ["git", "rev-parse", "HEAD"], cwd=repository, text=True + ).strip() + sources = repository / "LeanPool" + sources.mkdir() + (repository / "README.md").write_text("infrastructure change") + if content_change: + (sources / "New.lean").write_text("def value := 1") + subprocess.run(["git", "add", "."], cwd=repository, check=True) + subprocess.run( + [ + "git", + "-c", + "user.name=Test", + "-c", + "user.email=test@example.com", + "commit", + "-qm", + "PR change", + ], + cwd=repository, + check=True, + ) + head = subprocess.check_output( + ["git", "rev-parse", "HEAD"], cwd=repository, text=True + ).strip() + build = repository / ".lake/build/lib/lean/LeanPool" + build.mkdir() + shared = build / "Existing.olean" + shared.write_bytes(b"main build") + changed = build / "New.olean" + changed.write_bytes(b"PR build") + archive = repository / "projects.tar.gz" + ci_artifacts.pack_build(repository, archive, base=base, head=head) + with tarfile.open(archive) as contents: + names = contents.getnames() + assert shared.relative_to(repository).as_posix() not in names + assert (changed.relative_to(repository).as_posix() in names) == content_change + assert len(names) == (2 if content_change else 1) + shared.write_bytes(b"newer shared main build") + changed.unlink() + assert ci_artifacts.restore_build(repository, archive) + assert shared.read_bytes() == b"newer shared main build" + + assert changed.exists() == content_change + # Exact checkout identity still guards even empty project archives. + (repository / "README.md").write_text("later change") + subprocess.run(["git", "add", "."], cwd=repository, check=True) + subprocess.run( + [ + "git", + "-c", + "user.name=Test", + "-c", + "user.email=test@example.com", + "commit", + "-qm", + "later", + ], + cwd=repository, + check=True, + ) + assert not ci_artifacts.restore_build(repository, archive) + assert shared.read_bytes() == b"newer shared main build" + + +def test_project_overlay_rejects_unowned_outputs_before_install(repository): + """A bad overlay cannot replace an unrelated main-cache module.""" + destination = repository / "malformed.tar.gz" + identity = ci_artifacts.build_identity(repository) | {"projects": ["New"]} + with tarfile.open(destination, "w:gz") as archive: + payload = json.dumps(identity).encode() + entry = tarfile.TarInfo(ci_artifacts.MANIFEST_NAME) + entry.size = len(payload) + archive.addfile(entry, io.BytesIO(payload)) + for name in ("New", "Existing"): + entry = tarfile.TarInfo(f".lake/build/lib/lean/LeanPool/{name}.olean") + entry.size = 3 + archive.addfile(entry, io.BytesIO(b"bad")) + with pytest.raises(ValueError, match="Unexpected build archive member"): + ci_artifacts.restore_build(repository, destination) + assert not (repository / ".lake/build/lib/lean/LeanPool/New.olean").exists() + assert ( + repository / ".lake/build/lib/lean/LeanPool.olean" + ).read_bytes() == b"compiled" diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index da19e1114b..66d337c322 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -216,8 +216,8 @@ def test_required_scoped_checks_fail_closed_when_classification_fails() -> None: assert (process.returncode == 0) == accepted -def test_minimal_verifier_pr_has_an_explicit_full_build_producer(tmp_path): - """Cold minimal verification shares compilation while retaining its real gate.""" +def test_minimal_verifier_pr_has_an_explicit_project_build_producer(tmp_path): + """Minimal verification overlays only the PR's projects and retains its gate.""" lean = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] minimal = yaml.safe_load((WORKFLOWS / "exposition-verify.yml").read_text())["jobs"] assert "minimal_build" in lean["plan"]["outputs"] @@ -262,6 +262,9 @@ def test_minimal_verifier_pr_has_an_explicit_full_build_producer(tmp_path): ): assert "needs.plan.outputs.minimal_build == 'true'" in steps[producer]["if"] assert "github.event_name == 'pull_request'" in steps[producer]["if"] + package = steps["Package build for documentation"]["run"] + assert 'if [ "$BUILD_EVENT" = pull_request ]' in package + assert 'pack --base "$BASE_SHA" --head "$HEAD_SHA"' in package steps = {step.get("name"): step for step in minimal["verify"]["steps"]} reuse = steps["Reuse matching Lean CI build"] assert "github.event_name != 'pull_request'" not in reuse["if"] @@ -271,6 +274,30 @@ def test_minimal_verifier_pr_has_an_explicit_full_build_producer(tmp_path): assert "--baseline 214" in steps["Verify minimal files"]["run"] +def test_assembly_restores_projects_once_and_main_owns_full_cache(): + """Assembly recovers PR outputs once before fresh shard files are applied.""" + jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + assert not any( + "lean_pool.ci_pr_build" in step.get("run", "") + or "lean_pool.queue_build" in step.get("run", "") + for step in jobs["shard"]["steps"] + ) + steps = jobs["finalize"]["steps"] + names = [step.get("name") for step in steps] + assert names.index( + "Reuse compiled files from this PR's successful runs" + ) < names.index("Download shard build outputs") + assert names.index("Reuse successful queued PR builds") < names.index( + "Build project" + ) + for job in jobs.values(): + for step in job["steps"]: + if step.get("uses", "").startswith("actions/cache/save@"): + key = step["with"]["key"] + if key.startswith(("LeanPoolBuild-", "LeanDependencies-")): + assert "github.ref == 'refs/heads/main'" in step["if"] + + def test_minimal_build_wait_does_not_consume_verification_window() -> None: """A cold producer cannot use the verifier's six-hour execution allowance.""" jobs = yaml.safe_load((WORKFLOWS / "exposition-verify.yml").read_text())["jobs"] diff --git a/python/tests/test_ci_pr_build.py b/python/tests/test_ci_pr_build.py index b709dc7b88..94e701f232 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_pr_build, rebase_fastpath +from lean_pool import ci_artifacts, ci_pr_build, rebase_fastpath TOOLCHAIN = (Path(__file__).resolve().parents[2] / "lean-toolchain").read_text().strip() @@ -130,6 +130,30 @@ def _archive(root: Path, base: str, previous: str) -> tuple[Path, Path]: return archive, compiled +def test_lake_project_verifier_overlay_replays_without_recompilation(repository): + """A real project-only verifier artifact layers on main's unchanged traces.""" + root, base, head = repository + lake = _lake() + subprocess.run( + [str(lake), "build", "LeanPool.B"], cwd=root, check=True, capture_output=True + ) + shared = root / ".lake/build/lib/lean/LeanPool/A.olean" + shared_time = shared.stat().st_mtime_ns + archive = root / "verifier.tar.gz" + ci_artifacts.pack_build(root, archive, base=base, head=head) + build = root / ".lake/build" + for path in build.rglob("B.*"): + path.unlink() + assert ci_artifacts.restore_build(root, archive) + compiled = build / "lib/lean/LeanPool/B.olean" + compiled_time = compiled.stat().st_mtime_ns + subprocess.run( + [str(lake), "build", "LeanPool.B"], cwd=root, check=True, capture_output=True + ) + assert shared.stat().st_mtime_ns == shared_time + assert compiled.stat().st_mtime_ns == compiled_time + + def test_metadata_edit_reuses_build_without_skipping_validation( repository, monkeypatch ):