diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 13995e7a4b..54b8c99cd4 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -37,6 +37,7 @@ on: - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' - 'python/lean_pool/ci_cache.py' + - 'python/lean_pool/ci_pr_build.py' - 'python/lean_pool/ci_validation_artifacts.py' - 'python/lean_pool/rebase_fastpath.py' - 'python/pyproject.toml' @@ -66,6 +67,7 @@ on: - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' - 'python/lean_pool/ci_cache.py' + - 'python/lean_pool/ci_pr_build.py' - 'python/lean_pool/ci_validation_artifacts.py' - 'python/lean_pool/rebase_fastpath.py' - 'python/pyproject.toml' @@ -242,6 +244,13 @@ jobs: with: enable-cache: true + - name: Check compiled artifact dependency tracking with pinned Lean + env: + LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1' + run: >- + uv run --project python --group test pytest -q + python/tests/test_ci_pr_build.py -k 'test_lake_' + - name: Install Mathlib cache id: mathlib-cache run: | @@ -271,6 +280,21 @@ jobs: --repository "$REPOSITORY" --head "$BEFORE_SHA" --base "$GITHUB_SHA" fi + - 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 python3 -m lean_pool.ci_pr_build + --number "$PR_NUMBER" --branch "$PR_BRANCH" + --head "$PR_HEAD" --base "$PR_BASE" --current-run "$CURRENT_RUN" + - name: Build project id: compilation run: | diff --git a/python/lean_pool/ci_pr_build.py b/python/lean_pool/ci_pr_build.py new file mode 100644 index 0000000000..c6894ebf80 --- /dev/null +++ b/python/lean_pool/ci_pr_build.py @@ -0,0 +1,157 @@ +"""Warm ordinary PR builds without changing their compilation or validation gates.""" + +from __future__ import annotations + +import argparse +import logging +import os +import subprocess +import tarfile +import zipfile +from collections.abc import Iterator +from itertools import chain +from pathlib import Path +from urllib.parse import urlencode + +from lean_pool import rebase_fastpath + +LOGGER = logging.getLogger(__name__) +RECOVERY_ERRORS = ( + OSError, + ValueError, + KeyError, + subprocess.SubprocessError, + tarfile.TarError, + zipfile.BadZipFile, +) + + +def prior_runs( + repository: str, number: int, branch: str, current_run: int +) -> Iterator[dict]: + """Find successful runs of this PR; a later failed attempt supersedes its head.""" + seen = set() + page = 1 + while True: + query = urlencode( + {"event": "pull_request", "branch": branch, "per_page": 100, "page": page} + ) + runs = rebase_fastpath.github_json( + f"repos/{repository}/actions/workflows/lean_action_ci.yml/runs?{query}" + )["workflow_runs"] + for run in sorted(runs, key=lambda run: run["id"], reverse=True): + if run["id"] == current_run or not any( + pull.get("number") == number for pull in run.get("pull_requests", []) + ): + continue + if run["head_sha"] in seen: + continue + seen.add(run["head_sha"]) + if run.get("conclusion") == "success": + yield run + if len(runs) < 100: + return + page += 1 + + +def is_ancestor(root: Path, previous: str, head: str) -> bool: + """Use only the PR's own reachable history, including ordinary author commits.""" + return bool(rebase_fastpath.SHA.fullmatch(previous)) and ( + subprocess.run( + ["git", "merge-base", "--is-ancestor", previous, head], + cwd=root, + stdout=subprocess.DEVNULL, + stderr=subprocess.DEVNULL, + check=False, + ).returncode + == 0 + ) + + +def sources_match(root: Path, previous: str, base: str) -> bool: + """Avoid downloading large artifacts whose tracked Lean inputs already differ.""" + projects = rebase_fastpath._projects(root, base, previous) + if not all(rebase_fastpath.PROJECT.fullmatch(project) for project in projects): + return False + inputs = list(rebase_fastpath.PINNED_INPUTS) + for project in projects: + inputs.extend( + [f"LeanPool/{project}.lean", f":(glob)LeanPool/{project}/**/*.lean"] + ) + return ( + subprocess.run( + ["git", "diff", "--quiet", previous, "--", *inputs], + cwd=root, + check=False, + ).returncode + == 0 + ) + + +def restore_prior_build( + root: Path, + repository: str, + number: int, + branch: str, + head: str, + base: str, + current_run: int = 0, +) -> bool: + """Restore matching compiled files; Lake and every normal check still run.""" + if not all(rebase_fastpath.SHA.fullmatch(value) for value in (head, base)): + raise ValueError("invalid PR revisions") + candidates = ( + run + for run in prior_runs(repository, number, branch, current_run) + if is_ancestor(root, run["head_sha"], head) + ) + history = next(candidates, None) + if history is not None: + try: + rebase_fastpath.restore_new_main_projects( + root, repository, history["head_sha"], base, missing_only=True + ) + 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): + continue + try: + rebase_fastpath.restore(root, repository, run["id"], run["head_sha"]) + LOGGER.info("Restored matching PR build from 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") + return False + + +def main() -> None: + """Perform optional build reuse before the workflow's normal Lake invocation.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repository", default=os.environ.get("GITHUB_REPOSITORY", "")) + parser.add_argument("--number", type=int, required=True) + parser.add_argument("--branch", required=True) + parser.add_argument("--head", required=True) + parser.add_argument("--base", required=True) + parser.add_argument("--current-run", type=int, default=0) + arguments = parser.parse_args() + logging.basicConfig(level=logging.INFO, format="pr-build: %(message)s") + try: + restore_prior_build( + Path.cwd(), + arguments.repository, + arguments.number, + arguments.branch, + arguments.head, + arguments.base, + arguments.current_run, + ) + except RECOVERY_ERRORS: + LOGGER.exception("PR build reuse unavailable; normal compilation remains") + + +if __name__ == "__main__": + main() diff --git a/python/lean_pool/rebase_fastpath.py b/python/lean_pool/rebase_fastpath.py index 62df9b9682..cb1ea9804d 100644 --- a/python/lean_pool/rebase_fastpath.py +++ b/python/lean_pool/rebase_fastpath.py @@ -316,6 +316,23 @@ def pack(root: Path, base: str, head: str, output: Path) -> None: archive.add(path, arcname=relative.as_posix(), recursive=False) +def _restore_build_files( + root: Path, archive: tarfile.TarFile, members: list[tarfile.TarInfo] +) -> None: + build_parent = root / ".lake" + build_parent.mkdir(exist_ok=True) + # Stage on the destination filesystem, so publication uses atomic renames. + with tempfile.TemporaryDirectory( + prefix="lean-project-stage-", dir=build_parent + ) as name: + staging = Path(name) + archive.extractall(staging, members=members, filter="data") + for entry in members: + destination = root / entry.name + destination.parent.mkdir(parents=True, exist_ok=True) + 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.""" endpoint = f"repos/{repository}/actions/runs/{run_id}/artifacts?per_page=100" @@ -380,11 +397,11 @@ 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}") - archive.extractall(root, members=members, filter="data") + _restore_build_files(root, archive, members) def restore_new_main_projects( - root: Path, repository: str, previous: str, base: str + root: Path, repository: str, previous: str, base: str, *, missing_only: bool = False ) -> None: """Overlay merged PR artifacts before main's own large cache is published.""" old_base = git(root, "merge-base", previous, base) @@ -395,7 +412,15 @@ def restore_new_main_projects( parent = git(root, "rev-parse", f"{commit}^1") changed = paths(root, parent, commit) if not any( - path.startswith("LeanPool/") and path.endswith(".lean") for path in changed + path.startswith("LeanPool/") + and path.endswith(".lean") + and ( + not missing_only + or not (root / ".lake/build/lib/lean" / path) + .with_suffix(".olean") + .is_file() + ) + for path in changed ): continue try: diff --git a/python/tests/test_ci_pr_build.py b/python/tests/test_ci_pr_build.py new file mode 100644 index 0000000000..b709dc7b88 --- /dev/null +++ b/python/tests/test_ci_pr_build.py @@ -0,0 +1,433 @@ +"""Reusing compiled PR files must preserve ordinary builds and dependency failures.""" + +from __future__ import annotations + +import io +import json +import os +import shutil +import subprocess +import sys +import zipfile +from pathlib import Path + +import pytest + +from lean_pool import ci_pr_build, rebase_fastpath + +TOOLCHAIN = (Path(__file__).resolve().parents[2] / "lean-toolchain").read_text().strip() + + +def _lake() -> Path: + toolchain = TOOLCHAIN.replace("/", "--").replace(":", "---") + executable = Path.home() / ".elan/toolchains" / toolchain / "bin/lake" + if not executable.is_file(): + if os.environ.get("LEAN_POOL_REQUIRE_TEST_TOOLCHAIN") == "1": + pytest.fail(f"required pinned Lean toolchain unavailable: {TOOLCHAIN}") + pytest.skip("pinned Lean toolchain unavailable") + return executable + + +def _git(root: Path, *arguments: str) -> str: + return subprocess.check_output(["git", *arguments], cwd=root, text=True).strip() + + +def _commit(root: Path, message: str) -> str: + _git(root, "add", ".") + _git(root, "commit", "-qm", message) + return _git(root, "rev-parse", "HEAD") + + +@pytest.fixture +def repository(tmp_path: Path) -> tuple[Path, str, str]: + """A previous PR build remains unchanged while main edits its dependency.""" + root = tmp_path / "repo" + root.mkdir() + _git(root, "init", "-q", "-b", "main") + _git(root, "config", "user.email", "test@example.com") + _git(root, "config", "user.name", "Test") + (root / ".gitignore").write_text(".lake/\n*.tar.gz\n") + (root / "LeanPool").mkdir() + (root / "LeanPool/A.lean").write_text( + "module\n@[expose] public def value : Nat := 1\n" + ) + (root / "LeanPool/projects.yml").write_text("projects:\n - slug: a\n") + (root / "lean-toolchain").write_text(TOOLCHAIN + "\n") + (root / "lakefile.toml").write_text( + 'name = "fixture"\nrequiresModuleSystem = true\n' + '\n[[lean_lib]]\nname = "LeanPool"\n' + ) + (root / "lake-manifest.json").write_text( + json.dumps( + { + "version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "fixture", + "lakeDir": ".lake", + } + ) + ) + base = _commit(root, "base") + _git(root, "checkout", "-qb", "pr") + (root / "LeanPool/B.lean").write_text( + "module\npublic import LeanPool.A\n\n" + "public theorem value_one : value = 1 := rfl\n" + ) + (root / "LeanPool/projects.yml").write_text("projects:\n - slug: a\n - slug: b\n") + previous = _commit(root, "add B") + return root, base, previous + + +def _download(monkeypatch, archive: Path, previous: str) -> list[str]: + payload = io.BytesIO() + with zipfile.ZipFile(payload, "w") as wrapper: + wrapper.writestr(rebase_fastpath.ARCHIVE, archive.read_bytes()) + calls = [] + original_run = subprocess.run + + def api(endpoint): + calls.append(endpoint) + if "/runs?" in endpoint: + return { + "workflow_runs": [ + { + "id": 7, + "head_sha": previous, + "conclusion": "success", + "pull_requests": [{"number": 42}], + } + ] + } + if "/artifacts?" in endpoint: + return { + "artifacts": [ + {"id": 8, "name": rebase_fastpath.ARTIFACT, "expired": False} + ] + } + if endpoint.endswith("/pulls"): + return [] + pytest.fail(f"unexpected API request: {endpoint}") + + def run(command, **kwargs): + if command[:2] == ["gh", "api"]: + kwargs["stdout"].write(payload.getvalue()) + return subprocess.CompletedProcess(command, 0) + return original_run(command, **kwargs) + + monkeypatch.setattr(rebase_fastpath, "github_json", api) + monkeypatch.setattr(subprocess, "run", run) + return calls + + +def _archive(root: Path, base: str, previous: str) -> tuple[Path, Path]: + compiled = root / ".lake/build/lib/lean/LeanPool/B.olean" + compiled.parent.mkdir(parents=True, exist_ok=True) + compiled.write_text("prior compiled B") + archive = root / "build.tar.gz" + rebase_fastpath.pack(root, base, previous, archive) + compiled.unlink() + return archive, compiled + + +def test_metadata_edit_reuses_build_without_skipping_validation( + repository, monkeypatch +): + """Metadata edits retain compiled Lean files without writing validation receipts.""" + root, base, previous = repository + archive, compiled = _archive(root, base, previous) + (root / "LeanPool/projects.yml").write_text( + "projects:\n - slug: a\n - slug: b\n description: revised\n" + ) + head = _commit(root, "revise description") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + assert compiled.read_text() == "prior compiled B" + assert ( + (root / "LeanPool/projects.yml").read_text().endswith("description: revised\n") + ) + assert not (root / ".lake/validation-cache").exists() + + +@pytest.mark.parametrize( + "path", + [ + "LeanPool/B.lean", + "LeanPool/B/Added.lean", + "lean-toolchain", + "lake-manifest.json", + "lakefile.toml", + ], +) +def test_changed_source_or_settings_avoid_download(repository, monkeypatch, path): + """Changed sources and build settings fall back before any artifact download.""" + root, base, previous = repository + archive, compiled = _archive(root, base, previous) + target = root / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text("changed input\n") + head = _commit(root, "edit input") + calls = _download(monkeypatch, archive, previous) + assert not ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + assert not compiled.exists() + assert not any("/artifacts" in endpoint for endpoint in calls) + + +def test_latest_failed_attempt_and_other_pr_are_not_sources(monkeypatch): + """Only the latest successful attempt of each head belonging to this PR is used.""" + runs = [ + { + "id": 10, + "head_sha": "current", + "conclusion": None, + "pull_requests": [{"number": 42}], + }, + { + "id": 9, + "head_sha": "a", + "conclusion": "failure", + "pull_requests": [{"number": 42}], + }, + { + "id": 8, + "head_sha": "a", + "conclusion": "success", + "pull_requests": [{"number": 42}], + }, + { + "id": 7, + "head_sha": "b", + "conclusion": "success", + "pull_requests": [{"number": 99}], + }, + {"id": 6, "head_sha": "c", "conclusion": "success", "pull_requests": []}, + { + "id": 5, + "head_sha": "d", + "conclusion": "success", + "pull_requests": [{"number": 42}], + }, + ] + monkeypatch.setattr( + rebase_fastpath, "github_json", lambda _: {"workflow_runs": runs} + ) + assert list(ci_pr_build.prior_runs("owner/repo", 42, "pr", 10)) == [runs[-1]] + + +def test_unrelated_history_does_not_download(repository, monkeypatch): + """A successful run on unrelated history cannot supply compiled artifacts.""" + root, base, previous = repository + _git(root, "checkout", "-q", "main") + (root / "LeanPool/A.lean").write_text("module\n-- other branch\n") + unrelated = _commit(root, "other history") + _git(root, "checkout", "-q", "pr") + monkeypatch.setattr( + ci_pr_build, "prior_runs", lambda *args: [{"id": 7, "head_sha": unrelated}] + ) + monkeypatch.setattr( + rebase_fastpath, "restore", lambda *args: pytest.fail("unexpected download") + ) + assert not ci_pr_build.restore_prior_build( + root, "owner/repo", 42, "pr", previous, base + ) + + +def test_missing_artifact_preserves_existing_build(repository, monkeypatch): + """An expired or absent artifact leaves the restored main cache intact.""" + root, base, previous = repository + compiled = root / ".lake/build/lib/lean/LeanPool/B.olean" + compiled.parent.mkdir(parents=True) + compiled.write_text("existing build") + monkeypatch.setattr( + ci_pr_build, "prior_runs", lambda *args: [{"id": 7, "head_sha": previous}] + ) + monkeypatch.setattr(rebase_fastpath, "github_json", lambda _: {"artifacts": []}) + assert not ci_pr_build.restore_prior_build( + root, "owner/repo", 42, "pr", previous, base + ) + assert compiled.read_text() == "existing build" + + +def test_api_failure_leaves_normal_build_path(monkeypatch): + """Unavailable GitHub evidence cannot prevent the ordinary build from running.""" + monkeypatch.setattr( + sys, + "argv", + [ + "reuse", + "--number", + "42", + "--branch", + "pr", + "--head", + "a" * 40, + "--base", + "b" * 40, + ], + ) + + def unavailable(*args): + raise subprocess.CalledProcessError(1, "gh") + + monkeypatch.setattr(ci_pr_build, "prior_runs", unavailable) + ci_pr_build.main() + + +def test_lake_rebuilds_changed_dependency_and_rejects_invalid_proof( + repository, monkeypatch +): + """A real old olean cannot conceal a proof broken by a changed imported module.""" + 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") + _git(root, "checkout", "-q", "main") + (root / "LeanPool/A.lean").write_text( + "module\n@[expose] public def value : Nat := 2\n" + ) + changed_base = _commit(root, "change dependency") + _git(root, "checkout", "-q", "pr") + _git(root, "merge", "--no-edit", "main") + head = _git(root, "rev-parse", "HEAD") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build( + root, "owner/repo", 42, "pr", head, changed_base + ) + result = subprocess.run( + [str(lake), "build", "LeanPool.B"], cwd=root, capture_output=True, text=True + ) + assert result.returncode != 0 + assert "LeanPool.B" in result.stdout + result.stderr + 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 + 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") + (root / "LeanPool/projects.yml").write_text("projects: []\n") + head = _commit(root, "metadata update") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + compiled = root / ".lake/build/lib/lean/LeanPool/B.olean" + before = compiled.stat().st_mtime_ns + result = subprocess.run( + [str(lake), "build", "LeanPool.B"], cwd=root, capture_output=True, text=True + ) + assert result.returncode == 0, result.stdout + result.stderr + 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.""" + 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() + + +def test_broken_archive_preserves_existing_build(repository, monkeypatch): + """An unreadable project archive leaves existing compiled files intact.""" + root, base, previous = repository + archive, compiled = _archive(root, base, previous) + archive.write_bytes(b"broken archive") + compiled.write_text("existing build") + _download(monkeypatch, archive, previous) + assert not ci_pr_build.restore_prior_build( + root, "owner/repo", 42, "pr", previous, base + ) + assert compiled.read_text() == "existing build" + + +def test_main_recovery_failure_still_reuses_pr_build(repository, monkeypatch): + """Missing merged-project evidence does not block a matching own build.""" + root, base, previous = repository + archive, compiled = _archive(root, base, previous) + _download(monkeypatch, archive, previous) + + def unavailable(*args, **kwargs): + raise ValueError("merged artifact unavailable") + + monkeypatch.setattr(rebase_fastpath, "restore_new_main_projects", unavailable) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", previous, base) + assert compiled.read_text() == "prior compiled B" + + +def test_older_successful_run_found_on_later_page(monkeypatch): + """Long PR histories remain reusable without reviving a superseded failure.""" + newer = [ + { + "id": 1000 + number, + "head_sha": f"{number:040x}", + "conclusion": "failure", + "pull_requests": [{"number": 42}], + } + for number in range(100) + ] + older = [ + { + "id": 2, + "head_sha": newer[0]["head_sha"], + "conclusion": "success", + "pull_requests": [{"number": 42}], + }, + { + "id": 1, + "head_sha": "a" * 40, + "conclusion": "success", + "pull_requests": [{"number": 42}], + }, + ] + calls = [] + + def read(endpoint): + calls.append(endpoint) + return {"workflow_runs": older if "page=2" in endpoint else newer} + + monkeypatch.setattr(rebase_fastpath, "github_json", read) + assert list(ci_pr_build.prior_runs("owner/repo", 42, "pr", 0)) == [older[-1]] + assert len(calls) == 2 + + +def test_failed_extraction_never_overlays_partial_files(repository, monkeypatch): + """A late extraction error cannot overwrite any of the existing build.""" + root, base, previous = repository + archive, compiled = _archive(root, base, previous) + compiled.write_text("existing build") + _download(monkeypatch, archive, previous) + + def interrupted(archive, path, **kwargs): + partial = Path(path) / compiled.relative_to(root) + partial.parent.mkdir(parents=True, exist_ok=True) + partial.write_text("partial extraction") + raise OSError("simulated extraction failure") + + monkeypatch.setattr(rebase_fastpath.tarfile.TarFile, "extractall", interrupted) + assert not ci_pr_build.restore_prior_build( + root, "owner/repo", 42, "pr", previous, base + ) + assert compiled.read_text() == "existing build" + + +def test_required_toolchain_cannot_be_silently_skipped(monkeypatch): + """The real-Lean CI lane must fail if its installed toolchain is absent.""" + monkeypatch.setenv("LEAN_POOL_REQUIRE_TEST_TOOLCHAIN", "1") + monkeypatch.setattr(Path, "is_file", lambda path: False) + with pytest.raises(pytest.fail.Exception, match="required pinned Lean"): + _lake() diff --git a/python/tests/test_rebase_fastpath.py b/python/tests/test_rebase_fastpath.py index 2aa9cfb04f..7f33890568 100644 --- a/python/tests/test_rebase_fastpath.py +++ b/python/tests/test_rebase_fastpath.py @@ -331,11 +331,18 @@ def download( assert compiled.read_text() == "validated build" +@pytest.mark.parametrize("already_present", [False, True]) def test_new_main_project_reuses_its_merged_pr_artifact( - rebased: tuple[Path, str, str, str, str], monkeypatch: pytest.MonkeyPatch + rebased: tuple[Path, str, str, str, str], + monkeypatch: pytest.MonkeyPatch, + already_present: bool, ) -> None: """The main-cache gap need not force every waiting PR to compile the merger.""" root, _, previous, base, _ = rebased + if already_present: + compiled = root / ".lake/build/lib/lean/LeanPool/C.olean" + compiled.parent.mkdir(parents=True) + compiled.write_text("main cache already contains this project") merged_head = "c" * 40 restored = [] @@ -351,5 +358,9 @@ def read(endpoint: str) -> list[dict]: "restore", lambda *args: restored.append(args), ) - rebase_fastpath.restore_new_main_projects(root, "owner/repo", previous, base) - assert restored == [(root, "owner/repo", 11, merged_head)] + rebase_fastpath.restore_new_main_projects( + root, "owner/repo", previous, base, missing_only=True + ) + assert restored == ( + [] if already_present else [(root, "owner/repo", 11, merged_head)] + )