From 2e981bab879ec16ea14da423d18d55947cd0e5b2 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 6 Oct 2026 09:05:54 -0700 Subject: [PATCH 1/2] Reuse unchanged PR builds before ordinary CI compilation --- .github/workflows/lean_action_ci.yml | 17 ++ python/lean_pool/ci_pr_build.py | 145 +++++++++++ python/lean_pool/rebase_fastpath.py | 12 +- python/tests/test_ci_pr_build.py | 360 +++++++++++++++++++++++++++ python/tests/test_rebase_fastpath.py | 17 +- 5 files changed, 546 insertions(+), 5 deletions(-) create mode 100644 python/lean_pool/ci_pr_build.py create mode 100644 python/tests/test_ci_pr_build.py diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 13995e7a4b..9e82924e98 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' @@ -271,6 +273,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..f1de86876c --- /dev/null +++ b/python/lean_pool/ci_pr_build.py @@ -0,0 +1,145 @@ +"""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 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 +) -> list[dict]: + """Find successful runs of this PR; a later failed attempt supersedes its head.""" + query = urlencode({"event": "pull_request", "branch": branch, "per_page": 30}) + runs = rebase_fastpath.github_json( + f"repos/{repository}/actions/workflows/lean_action_ci.yml/runs?{query}" + )["workflow_runs"] + latest = {} + 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 + latest.setdefault(run["head_sha"], run) + return [run for run in latest.values() if run.get("conclusion") == "success"] + + +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 = prior_runs(repository, number, branch, current_run) + history = next( + (run for run in candidates if is_ancestor(root, run["head_sha"], head)), 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 candidates: + if not is_ancestor(root, run["head_sha"], head) or 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..2be346f116 100644 --- a/python/lean_pool/rebase_fastpath.py +++ b/python/lean_pool/rebase_fastpath.py @@ -384,7 +384,7 @@ def restore(root: Path, repository: str, run_id: int, previous_head: str) -> Non 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 +395,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..5bda584c50 --- /dev/null +++ b/python/tests/test_ci_pr_build.py @@ -0,0 +1,360 @@ +"""Reusing compiled PR files must preserve ordinary builds and dependency failures.""" + +from __future__ import annotations + +import io +import json +import shutil +import subprocess +import sys +import zipfile +from pathlib import Path + +import pytest + +from lean_pool import ci_pr_build, rebase_fastpath + + +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("leanprover/lean4:v4.35.0-rc3\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 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 = Path.home() / ".elan/toolchains/leanprover--lean4---v4.35.0-rc3/bin/lake" + if not lake.is_file(): + pytest.skip("pinned Lean toolchain unavailable") + 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 = Path.home() / ".elan/toolchains/leanprover--lean4---v4.35.0-rc3/bin/lake" + if not lake.is_file(): + pytest.skip("pinned Lean toolchain unavailable") + 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" 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)] + ) From 15dcc57b1b16b882df83aad53c0e0ab7358a9eff Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 6 Oct 2026 09:24:33 -0700 Subject: [PATCH 2/2] Harden artifact restoration and run dependency checks with pinned Lean --- .github/workflows/lean_action_ci.yml | 7 +++ python/lean_pool/ci_pr_build.py | 52 +++++++++------- python/lean_pool/rebase_fastpath.py | 19 +++++- python/tests/test_ci_pr_build.py | 89 +++++++++++++++++++++++++--- 4 files changed, 138 insertions(+), 29 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 9e82924e98..54b8c99cd4 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -244,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: | diff --git a/python/lean_pool/ci_pr_build.py b/python/lean_pool/ci_pr_build.py index f1de86876c..c6894ebf80 100644 --- a/python/lean_pool/ci_pr_build.py +++ b/python/lean_pool/ci_pr_build.py @@ -8,6 +8,8 @@ import subprocess import tarfile import zipfile +from collections.abc import Iterator +from itertools import chain from pathlib import Path from urllib.parse import urlencode @@ -26,20 +28,30 @@ def prior_runs( repository: str, number: int, branch: str, current_run: int -) -> list[dict]: +) -> Iterator[dict]: """Find successful runs of this PR; a later failed attempt supersedes its head.""" - query = urlencode({"event": "pull_request", "branch": branch, "per_page": 30}) - runs = rebase_fastpath.github_json( - f"repos/{repository}/actions/workflows/lean_action_ci.yml/runs?{query}" - )["workflow_runs"] - latest = {} - 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 - latest.setdefault(run["head_sha"], run) - return [run for run in latest.values() if run.get("conclusion") == "success"] + 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: @@ -88,10 +100,12 @@ def restore_prior_build( """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 = prior_runs(repository, number, branch, current_run) - history = next( - (run for run in candidates if is_ancestor(root, run["head_sha"], head)), None + 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( @@ -99,10 +113,8 @@ def restore_prior_build( ) except RECOVERY_ERRORS: LOGGER.info("Merged project reuse unavailable; checking the PR's build") - for run in candidates: - if not is_ancestor(root, run["head_sha"], head) or not sources_match( - root, run["head_sha"], base - ): + 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"]) diff --git a/python/lean_pool/rebase_fastpath.py b/python/lean_pool/rebase_fastpath.py index 2be346f116..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,7 +397,7 @@ 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( diff --git a/python/tests/test_ci_pr_build.py b/python/tests/test_ci_pr_build.py index 5bda584c50..b709dc7b88 100644 --- a/python/tests/test_ci_pr_build.py +++ b/python/tests/test_ci_pr_build.py @@ -4,6 +4,7 @@ import io import json +import os import shutil import subprocess import sys @@ -14,6 +15,18 @@ 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() @@ -39,7 +52,7 @@ def repository(tmp_path: Path) -> tuple[Path, str, str]: "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("leanprover/lean4:v4.35.0-rc3\n") + (root / "lean-toolchain").write_text(TOOLCHAIN + "\n") (root / "lakefile.toml").write_text( 'name = "fixture"\nrequiresModuleSystem = true\n' '\n[[lean_lib]]\nname = "LeanPool"\n' @@ -198,7 +211,7 @@ def test_latest_failed_attempt_and_other_pr_are_not_sources(monkeypatch): monkeypatch.setattr( rebase_fastpath, "github_json", lambda _: {"workflow_runs": runs} ) - assert ci_pr_build.prior_runs("owner/repo", 42, "pr", 10) == [runs[-1]] + assert list(ci_pr_build.prior_runs("owner/repo", 42, "pr", 10)) == [runs[-1]] def test_unrelated_history_does_not_download(repository, monkeypatch): @@ -265,9 +278,7 @@ def test_lake_rebuilds_changed_dependency_and_rejects_invalid_proof( ): """A real old olean cannot conceal a proof broken by a changed imported module.""" root, base, previous = repository - lake = Path.home() / ".elan/toolchains/leanprover--lean4---v4.35.0-rc3/bin/lake" - if not lake.is_file(): - pytest.skip("pinned Lean toolchain unavailable") + lake = _lake() subprocess.run( [str(lake), "build", "LeanPool.B"], cwd=root, check=True, capture_output=True ) @@ -297,9 +308,7 @@ def test_lake_rebuilds_changed_dependency_and_rejects_invalid_proof( def test_lake_keeps_unchanged_proof_after_metadata_edit(repository, monkeypatch): """Lake accepts matching artifacts without recompiling unchanged proofs.""" root, base, previous = repository - lake = Path.home() / ".elan/toolchains/leanprover--lean4---v4.35.0-rc3/bin/lake" - if not lake.is_file(): - pytest.skip("pinned Lean toolchain unavailable") + lake = _lake() subprocess.run( [str(lake), "build", "LeanPool.B"], cwd=root, check=True, capture_output=True ) @@ -358,3 +367,67 @@ def unavailable(*args, **kwargs): 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()