Reuse main build caches with project-only PR artifacts

.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')

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,16 +217,20 @@ 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)
         has_files |= member.isfile()
         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,

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"