From 1c88eb8279a39f9cce915bb38466d639d58a4508 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 28 Sep 2026 01:57:18 -0500 Subject: [PATCH] ci: reuse validated PR builds after mechanical rebases --- .github/workflows/docs.yml | 31 +- .github/workflows/lean_action_ci.yml | 201 +++++++++++- python/lean_pool/quality.py | 58 +++- python/lean_pool/rebase_fastpath.py | 474 +++++++++++++++++++++++++++ python/tests/test_rebase_fastpath.py | 355 ++++++++++++++++++++ 5 files changed, 1100 insertions(+), 19 deletions(-) create mode 100644 python/lean_pool/rebase_fastpath.py create mode 100644 python/tests/test_rebase_fastpath.py diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index f1807d11f7..43fad47bbc 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -17,6 +17,7 @@ on: - 'python/lean_pool/challenge.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' + - 'python/lean_pool/rebase_fastpath.py' - 'scripts/exposition/**' - '.github/workflows/docs.yml' pull_request: @@ -41,6 +42,7 @@ on: - 'python/lean_pool/challenge.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' + - 'python/lean_pool/rebase_fastpath.py' - 'scripts/exposition/**' - '.github/workflows/notice.yml' - '.github/workflows/docs.yml' @@ -73,6 +75,7 @@ jobs: name: Documentation preflight outputs: readme_only: ${{ steps.scope.outputs.readme_only }} + rebase_only: ${{ steps.rebase.outputs.rebase_only }} steps: - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd @@ -97,6 +100,22 @@ jobs: echo "readme_only=$readme_only" >> "$GITHUB_OUTPUT" echo "README-only change: $readme_only" + - name: Verify prior documentation preflight for a content-only rebase + id: rebase + if: github.event_name == 'pull_request' && steps.scope.outputs.readme_only != 'true' + env: + GH_TOKEN: ${{ github.token }} + REPOSITORY: ${{ github.repository }} + PR_NUMBER: ${{ github.event.pull_request.number }} + HEAD_SHA: ${{ github.event.pull_request.head.sha }} + BASE_SHA: ${{ github.event.pull_request.base.sha }} + run: | + decision=$(PYTHONPATH=python python3 -m lean_pool.rebase_fastpath decide \ + --workflow docs.yml --repository "$REPOSITORY" --number "$PR_NUMBER" \ + --head "$HEAD_SHA" --base "$BASE_SHA") + echo "rebase_only=$(echo "$decision" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" >> "$GITHUB_OUTPUT" + echo "$decision" + # docbuild deliberately reuses the root workspace's compiled artifacts. # Fail before restoring anything if those workspaces ever diverge. - name: Check documentation workspace compatibility @@ -126,7 +145,7 @@ jobs: # Stable dependencies are shared with CI without a new copy per commit. - name: Restore Lean dependencies id: dependency-cache - if: steps.scope.outputs.readme_only != 'true' + if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | @@ -135,7 +154,7 @@ jobs: key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - name: Install Lean - if: steps.scope.outputs.readme_only != 'true' + if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: auto-config: false @@ -146,7 +165,7 @@ jobs: # oleans match the current manifest. `cache get` is incremental, so run it # unconditionally and then verify the checkout revision. - name: Install and verify Mathlib cache - if: steps.scope.outputs.readme_only != 'true' + if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' run: | set -euo pipefail ~/.elan/bin/lake exe cache get @@ -158,9 +177,13 @@ jobs: fi - name: Check generated roots - if: steps.scope.outputs.readme_only != 'true' + if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' run: ~/.elan/bin/lake exe mk_all --check + - name: Check regenerated LeanPool root without Lean + if: steps.rebase.outputs.rebase_only == 'true' + run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath check-index + # Runs in parallel with the doc-gen4 build; its (small) artifact is merged # into the Pages tree by the `deploy` job. Restores the root build cache but # never saves it — Lean Action CI owns that cache, while the documentation diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index ac0e261afc..a70d46cd1d 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -7,6 +7,8 @@ name: Lean Action CI # protected `Build project` check without spending hours rebuilding Lean. # - `single`: the classic one-job pipeline. This is the fast path for the # common case — a PR that adds or edits a project or three. +# - `rebase`: reuse an earlier green PR build after the automatic merge of +# independent pool content, then build the combined root and check metadata. # - `sharded`: for the runs that take hours serially (cold cache, # toolchain/manifest bump, refactors touching many projects), the dirty # projects are bin-packed into parallel `shard` build jobs. Pool projects @@ -36,6 +38,7 @@ on: - 'python/lean_pool/quality.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' + - 'python/lean_pool/rebase_fastpath.py' - 'python/pyproject.toml' - 'python/uv.lock' - 'scripts/nolints-style.txt' @@ -64,6 +67,7 @@ on: - 'python/lean_pool/quality.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' + - 'python/lean_pool/rebase_fastpath.py' - 'python/pyproject.toml' - 'python/uv.lock' - 'scripts/nolints-style.txt' @@ -88,6 +92,7 @@ permissions: contents: read pages: write id-token: write + actions: read jobs: plan: @@ -96,6 +101,8 @@ jobs: outputs: mode: ${{ steps.plan.outputs.mode }} matrix: ${{ steps.plan.outputs.matrix }} + reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }} + previous_head: ${{ steps.plan.outputs.previous_head }} steps: - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd @@ -122,6 +129,10 @@ jobs: BEFORE_SHA: ${{ github.event.before }} FORCE_FULL: ${{ inputs.force_full }} CACHE_MATCHED: ${{ steps.lake-cache.outputs.cache-matched-key }} + GH_TOKEN: ${{ github.token }} + REPOSITORY: ${{ github.repository }} + PR_NUMBER: ${{ github.event.pull_request.number }} + PR_HEAD: ${{ github.event.pull_request.head.sha }} run: | set -euo pipefail diff_available=true @@ -151,10 +162,26 @@ jobs: plan=$(CHANGED_FILES_PATH="$changed_files" DIFF_AVAILABLE="$diff_available" \ COLD="$cold" FORCE_FULL="$FORCE_FULL" \ python3 scripts/ci/plan-build-shards.py) + reuse_run_id="" + previous_head="" + if [ "$EVENT_NAME" = "pull_request" ] && [ "$FORCE_FULL" != "true" ]; then + reuse=$(PYTHONPATH=python python3 -m lean_pool.rebase_fastpath decide \ + --repository "$REPOSITORY" --number "$PR_NUMBER" \ + --head "$PR_HEAD" --base "$BASE_SHA") + if [ "$(echo "$reuse" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" = true ]; then + reuse_run_id=$(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["run_id"])') + previous_head=$(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["previous_head"])') + plan='{"mode":"rebase","matrix":{"include":[{"shard":"00","projects":""}]}}' + else + echo "Rebase reuse unavailable: $(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["reason"])')" + fi + fi echo "Plan: $plan" { echo "mode=$(echo "$plan" | python3 -c 'import json,sys; print(json.load(sys.stdin)["mode"])')" echo "matrix=$(echo "$plan" | python3 -c 'import json,sys; print(json.dumps(json.load(sys.stdin)["matrix"]))')" + echo "reuse_run_id=$reuse_run_id" + echo "previous_head=$previous_head" } >> "$GITHUB_OUTPUT" # The single-job pipeline is the fast path for ordinary PRs. @@ -276,6 +303,25 @@ jobs: cd python uv run python -m lean_pool.validation_cache quality --repo .. + - name: Package PR project build for later rebases + if: github.event_name == 'pull_request' + continue-on-error: true + env: + BASE_SHA: ${{ github.event.pull_request.base.sha }} + HEAD_SHA: ${{ github.event.pull_request.head.sha }} + run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA" + + - name: Retain PR project build + if: github.event_name == 'pull_request' + continue-on-error: true + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: rebase-project-build + path: rebase-project-build.tar.gz + if-no-files-found: error + compression-level: 0 + retention-days: 14 + - name: Save project validation # Successful receipts are tiny; retain PR results across registry rebases. uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -535,6 +581,25 @@ jobs: cd python uv run python -m lean_pool.validation_cache quality --repo .. + - name: Package PR project build for later rebases + if: github.event_name == 'pull_request' + continue-on-error: true + env: + BASE_SHA: ${{ github.event.pull_request.base.sha }} + HEAD_SHA: ${{ github.event.pull_request.head.sha }} + run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA" + + - name: Retain PR project build + if: github.event_name == 'pull_request' + continue-on-error: true + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: rebase-project-build + path: rebase-project-build.tar.gz + if-no-files-found: error + compression-level: 0 + retention-days: 14 + - name: Save project validation # Successful receipts are tiny; retain PR results across registry rebases. uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -558,10 +623,140 @@ jobs: path: .lake/build key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} + # Reuse the prior green project's compiled modules and current main's cache. + # A missing artifact falls back to the full validation sequence in this job. + rebase: + needs: plan + if: needs.plan.outputs.mode == 'rebase' + runs-on: ubuntu-latest + name: Check rebased root + steps: + - name: Checkout project + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + fetch-depth: 0 + + - name: Restore Lean dependencies + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: | + ~/.elan + .lake/packages + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore current main build + id: main-build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.event.pull_request.base.sha }} + restore-keys: | + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- + + - name: Reuse newly merged projects while the main cache warms + if: steps.main-build.outputs.cache-hit != 'true' + continue-on-error: true + env: + GH_TOKEN: ${{ github.token }} + REPOSITORY: ${{ github.repository }} + PREVIOUS_HEAD: ${{ needs.plan.outputs.previous_head }} + BASE_SHA: ${{ github.event.pull_request.base.sha }} + run: >- + PYTHONPATH=python python3 -m lean_pool.rebase_fastpath restore-main + --repository "$REPOSITORY" --head "$PREVIOUS_HEAD" --base "$BASE_SHA" + + - name: Restore previously validated PR modules + id: project-build + continue-on-error: true + env: + GH_TOKEN: ${{ github.token }} + RUN_ID: ${{ needs.plan.outputs.reuse_run_id }} + PREVIOUS_HEAD: ${{ needs.plan.outputs.previous_head }} + REPOSITORY: ${{ github.repository }} + run: >- + PYTHONPATH=python python3 -m lean_pool.rebase_fastpath restore + --repository "$REPOSITORY" --run-id "$RUN_ID" --head "$PREVIOUS_HEAD" + + - name: Install Lean + uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 + with: + auto-config: false + use-github-cache: false + use-mathlib-cache: false + + - name: Install uv + uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff + with: + enable-cache: true + + - name: Install Mathlib cache + run: | + if [ ! -d ".lake/packages/mathlib" ]; then + ~/.elan/bin/lake exe cache get + fi + + - name: Check generated index + run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath check-index + + - name: Build combined Lean root + run: | + set -euo pipefail + ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log + if grep -nE '(^|: )warning:' lean-build.log; then + echo "::error::Lean build emitted warnings; fix them before merging." + exit 1 + fi + + - name: Install validation dependencies + run: cd python && uv sync --locked + + - name: Validate combined repository metadata + if: steps.project-build.outcome == 'success' + run: cd python && uv run python -m lean_pool.quality --repo .. --static-only + + - name: Restore validation cache for full fallback + if: steps.project-build.outcome != 'success' + 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: Full validation when the prior artifact is unavailable + if: steps.project-build.outcome != 'success' + run: | + set -euo pipefail + ./scripts/ci/build-challenges.sh + (cd python && uv run python -m lean_pool.validation_cache lint --repo ..) + ~/.elan/bin/lake exe runLinter Challenge + ~/.elan/bin/lake exe runLinter Solution + ~/.elan/bin/lake exe lint-style LeanPool + ~/.elan/bin/lake exe lint-style Challenge + ~/.elan/bin/lake exe lint-style Solution + (cd python && uv run python -m lean_pool.validation_cache quality --repo ..) + + - name: Package PR project build for later rebases + continue-on-error: true + env: + BASE_SHA: ${{ github.event.pull_request.base.sha }} + HEAD_SHA: ${{ github.event.pull_request.head.sha }} + run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA" + + - name: Retain PR project build + continue-on-error: true + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: rebase-project-build + path: rebase-project-build.tar.gz + if-no-files-found: error + compression-level: 0 + retention-days: 14 + # Single overall verdict under the check name the one-job workflow used, # so nothing watching "Build project" needs to change. gate: - needs: [plan, build, shard, finalize] + needs: [plan, build, shard, finalize, rebase] if: always() runs-on: ubuntu-latest name: Build project @@ -573,6 +768,7 @@ jobs: BUILD_RESULT: ${{ needs.build.result }} SHARD_RESULT: ${{ needs.shard.result }} FINALIZE_RESULT: ${{ needs.finalize.result }} + REBASE_RESULT: ${{ needs.rebase.result }} run: | set -euo pipefail echo "plan=$PLAN_RESULT mode=$MODE build=$BUILD_RESULT shard=$SHARD_RESULT finalize=$FINALIZE_RESULT" @@ -584,6 +780,9 @@ jobs: skip) echo "No Lean build inputs changed." ;; + rebase) + [ "$REBASE_RESULT" = "success" ] || { echo "::error::Rebase validation failed."; exit 1; } + ;; single) [ "$BUILD_RESULT" = "success" ] || { echo "::error::Build failed."; exit 1; } ;; diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index faf5f5d373..4044e249c0 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -1123,7 +1123,10 @@ def _load_projects_yaml( def _check_projects( - root: Path, validation_cache: ValidationCache | None = None + root: Path, + validation_cache: ValidationCache | None = None, + *, + skip_declarations: bool = False, ) -> list[_QualityError]: data, errors = _load_projects_yaml(root) if data is None: @@ -1146,7 +1149,16 @@ def _check_projects( return errors for index, project in enumerate(projects, start=1): - errors.extend(_check_project(root, path, index, project, validation_cache)) + errors.extend( + _check_project( + root, + path, + index, + project, + validation_cache, + skip_declarations=skip_declarations, + ) + ) return errors @@ -1243,6 +1255,8 @@ def _check_project( index: int, project: Any, validation_cache: ValidationCache | None = None, + *, + skip_declarations: bool = False, ) -> list[_QualityError]: if not isinstance(project, dict): return [_QualityError(path, 1, f"project #{index} must be a mapping")] @@ -1253,17 +1267,18 @@ def _check_project( return errors entry_path = _module_to_path(root, project["entry_module"]) - if validation_cache is None: - errors.extend(_check_project_declarations(root, path, project)) - else: - errors.extend( - validation_cache.check( - "declarations", - [project["entry_module"]], - lambda: _check_project_declarations(root, path, project), - metadata=project, + if not skip_declarations: + if validation_cache is None: + errors.extend(_check_project_declarations(root, path, project)) + else: + errors.extend( + validation_cache.check( + "declarations", + [project["entry_module"]], + lambda: _check_project_declarations(root, path, project), + metadata=project, + ) ) - ) errors.extend(_check_project_card(entry_path, path, project)) return errors @@ -1859,6 +1874,7 @@ def run_checks( root: Path, *, skip_lean_axioms: bool = False, + skip_project_declarations: bool = False, validation_cache: ValidationCache | None = None, ) -> list[_QualityError]: """Run all deterministic quality checks.""" @@ -1873,7 +1889,11 @@ def run_checks( _check_challenges, ] errors = [error for check in checks for error in check(root)] - errors.extend(_check_projects(root, validation_cache)) + errors.extend( + _check_projects( + root, validation_cache, skip_declarations=skip_project_declarations + ) + ) if not skip_lean_axioms: if validation_cache is None: errors.extend(_check_axioms(root)) @@ -1926,6 +1946,12 @@ def _parse_args(argv: list[str]) -> argparse.Namespace: help="Skip the Lean subprocess used for #print axioms and the " "option-manipulation environment audit.", ) + parser.add_argument( + "--static-only", + action="store_true", + help="Run repository and card checks without Lean subprocesses " + "(for a verified rebase).", + ) parser.add_argument( "--write-project-cards", action="store_true", @@ -1948,7 +1974,11 @@ def main(argv: list[str] | None = None) -> int: if args.write_challenge_cards: _write_challenge_cards(root) - errors = run_checks(root, skip_lean_axioms=args.skip_lean_axioms) + errors = run_checks( + root, + skip_lean_axioms=args.skip_lean_axioms or args.static_only, + skip_project_declarations=args.static_only, + ) if errors: for error in errors: print(error.format(root), file=sys.stderr) diff --git a/python/lean_pool/rebase_fastpath.py b/python/lean_pool/rebase_fastpath.py new file mode 100644 index 0000000000..2fd9533602 --- /dev/null +++ b/python/lean_pool/rebase_fastpath.py @@ -0,0 +1,474 @@ +"""Reuse a green PR build after an automatic, content-only merge of main. + +The fast path is deliberately narrow. It requires a successful earlier run on +the first parent of the rebase merge, unchanged PR-owned project sources, and +only LeanPool content added by main. Everything else uses ordinary CI. +""" + +from __future__ import annotations + +import argparse +import hashlib +import io +import json +import os +import re +import shutil +import subprocess +import sys +import tarfile +import tempfile +import zipfile +from pathlib import Path, PurePosixPath +from typing import Any +from urllib.parse import urlencode + +ARTIFACT = "rebase-project-build" +ARCHIVE = f"{ARTIFACT}.tar.gz" +MANIFEST = "rebase-build-manifest.json" +REGISTRY = "LeanPool/projects.yml" +INDEX = "LeanPool.lean" +PINNED_INPUTS = ("lean-toolchain", "lake-manifest.json", "lakefile.toml") +SHA = re.compile(r"[0-9a-f]{40}\Z") +PROJECT = re.compile(r"[A-Za-z][A-Za-z0-9_]*\Z") +CARD = re.compile(r"^ - slug: ([A-Za-z0-9_-]+)[ \t]*$", re.MULTILINE) + + +def git(root: Path, *arguments: str) -> str: + """Run a Git read in the checkout.""" + return subprocess.check_output(["git", *arguments], cwd=root, text=True).strip() + + +def paths(root: Path, before: str, after: str, *, merge_base: bool = False) -> set[str]: + """List changed paths using NUL delimiters and no rename inference.""" + separator = "..." if merge_base else ".." + output = subprocess.check_output( + [ + "git", + "diff", + "--name-only", + "-z", + "--no-renames", + f"{before}{separator}{after}", + ], + cwd=root, + ) + return {os.fsdecode(path) for path in output.split(b"\0") if path} + + +def github_json(endpoint: str) -> Any: + """Read repository metadata through the runner's authenticated GitHub CLI.""" + return json.loads( + subprocess.check_output(["gh", "api", endpoint], text=True, timeout=60) + ) + + +def _content_path(path: str) -> bool: + return path in {INDEX, REGISTRY} or ( + path.startswith("LeanPool/") and path.endswith(".lean") + ) + + +def _main_path(path: str) -> bool: + """Allow generated metadata alongside independently verified pool content.""" + return _content_path(path) or path in {"README.md", "NOTICE"} + + +def _exists_at(root: Path, revision: str, path: str) -> bool: + """Check whether a file already existed before main advanced.""" + return ( + subprocess.run( + ["git", "cat-file", "-e", f"{revision}:{path}"], + cwd=root, + capture_output=True, + check=False, + ).returncode + == 0 + ) + + +def _registry_cards(root: Path, revision: str) -> dict[str, str]: + """Split the repository's slug-first registry, rejecting unfamiliar layouts.""" + source = git(root, "show", f"{revision}:{REGISTRY}") + if not source.startswith("projects:\n"): + raise ValueError("unrecognized project registry layout") + matches = list(CARD.finditer(source)) + if not matches or source[: matches[0].start()] != "projects:\n": + raise ValueError("unrecognized project registry cards") + cards = {} + for index, match in enumerate(matches): + end = matches[index + 1].start() if index + 1 < len(matches) else len(source) + slug = match.group(1) + if slug in cards: + raise ValueError("duplicate project card") + cards[slug] = source[match.start() : end].rstrip("\n") + return cards + + +def _registry_rebased( + root: Path, old_base: str, previous: str, base: str, head: str +) -> bool: + """Require current cards to equal the new main plus unchanged PR additions.""" + before = _registry_cards(root, old_base) + old_pr = _registry_cards(root, previous) + main = _registry_cards(root, base) + current = _registry_cards(root, head) + if any(old_pr.get(slug) != card for slug, card in before.items()): + return False + added = {slug: card for slug, card in old_pr.items() if slug not in before} + if set(added) & set(main): + return False + return current == (main | added) + + +def _previous_head(root: Path, head: str, base: str) -> str | None: + """Accept the bot's merge, optionally followed by one index-only commit.""" + current = head + for _ in range(2): + parents = git(root, "rev-list", "--parents", "-n", "1", current).split() + if len(parents) == 3: + return parents[1] if parents[2] == base else None + if len(parents) != 2 or paths(root, parents[1], current) != {INDEX}: + return None + current = parents[1] + return None + + +def _successful_run( + repository: str, + workflow: str, + number: int, + head: str, + *, + merged: bool = False, +) -> dict | None: + query = urlencode({"event": "pull_request", "head_sha": head, "per_page": 100}) + endpoint = f"repos/{repository}/actions/workflows/{workflow}/runs?{query}" + runs = github_json(endpoint)["workflow_runs"] + matches = [ + run + for run in runs + if run.get("head_sha") == head + # GitHub clears pull_requests on workflow runs after that PR merges. + # The caller verifies the commit-to-PR association for merged runs. + and ( + merged + or any( + pull.get("number") == number for pull in run.get("pull_requests", []) + ) + ) + ] + if not matches: + return None + latest = max(matches, key=lambda run: run["id"]) + return latest if latest.get("conclusion") == "success" else None + + +def _has_build_artifact(repository: str, run_id: int) -> bool: + endpoint = f"repos/{repository}/actions/runs/{run_id}/artifacts?per_page=100" + return any( + artifact["name"] == ARTIFACT and not artifact["expired"] + for artifact in github_json(endpoint)["artifacts"] + ) + + +def decision( + root: Path, repository: str, workflow: str, number: int, head: str, base: str +) -> dict: + """Return a verified reuse decision; uncertainty always selects full CI.""" + result = {"eligible": False, "reason": "not a verified content-only rebase"} + if workflow not in {"lean_action_ci.yml", "docs.yml"} or not all( + SHA.fullmatch(value) for value in (head, base) + ): + return result + previous = _previous_head(root, head, base) + if previous is None: + return result + run = _successful_run(repository, workflow, number, previous) + if run is None: + return {**result, "reason": "no successful earlier PR run"} + # The Actions API's embedded pull_request.base.sha follows the *current* + # PR base, even for an older run. Git ancestry is the stable source here. + old_base = git(root, "merge-base", previous, base) + if not SHA.fullmatch(old_base): + return result + if subprocess.run( + ["git", "merge-base", "--is-ancestor", old_base, base], cwd=root, check=False + ).returncode: + return result + main_delta = paths(root, old_base, base) + if not main_delta or not all(map(_main_path, main_delta)): + return {**result, "reason": "main changed shared build or validation inputs"} + if any( + path != INDEX and path.endswith(".lean") and _exists_at(root, old_base, path) + for path in main_delta + ): + return {**result, "reason": "main edited existing Lean sources"} + old_pr = paths(root, old_base, previous, merge_base=True) + new_pr = paths(root, base, head, merge_base=True) + if not all(map(_content_path, old_pr | new_pr)): + return result + old_owned = old_pr - {INDEX, REGISTRY} + new_owned = new_pr - {INDEX, REGISTRY} + if old_owned != new_owned or old_owned & main_delta: + return {**result, "reason": "PR-owned Lean sources changed"} + for path in old_owned: + if git(root, "rev-parse", f"{previous}:{path}") != git( + root, "rev-parse", f"{head}:{path}" + ): + return {**result, "reason": "PR-owned Lean sources changed"} + if not _registry_rebased(root, old_base, previous, base, head): + return {**result, "reason": "project cards changed beyond the merge"} + if workflow == "lean_action_ci.yml" and not _has_build_artifact( + repository, run["id"] + ): + return {**result, "reason": "prior PR build artifact unavailable"} + return { + "eligible": True, + "reason": "verified rebase", + "run_id": run["id"], + "previous_head": previous, + } + + +def check_index(root: Path) -> bool: + """Check the generated root without starting Lean or downloading Mathlib.""" + pool = root / "LeanPool" + modules = sorted( + "LeanPool." + + path.relative_to(pool).with_suffix("").as_posix().replace("/", ".") + for path in pool.rglob("*.lean") + ) + expected = "module -- shake: keep-all --deprecated_module: ignore\n\n" + expected += "".join(f"public import {module}\n" for module in modules) + return (root / INDEX).read_text(encoding="utf-8") == expected + + +def _projects(root: Path, base: str, head: str) -> list[str]: + return sorted( + { + path.split("/")[1].removesuffix(".lean") + for path in paths(root, base, head, merge_base=True) + if path.startswith("LeanPool/") and path.endswith(".lean") + } + ) + + +def _source_hashes(root: Path, projects: list[str]) -> dict[str, str]: + result = {} + for project in projects: + for path in sorted((root / "LeanPool").glob(f"{project}.lean")): + result[path.relative_to(root).as_posix()] = hashlib.sha256( + path.read_bytes() + ).hexdigest() + for path in sorted((root / "LeanPool" / project).rglob("*.lean")): + result[path.relative_to(root).as_posix()] = hashlib.sha256( + path.read_bytes() + ).hexdigest() + return result + + +def _build_file_for_project(relative: PurePosixPath, projects: set[str]) -> bool: + parts = relative.parts + if parts[:4] == (".lake", "build", "ir", "LeanPool"): + module = parts[4:] + elif parts[:5] == (".lake", "build", "lib", "lean", "LeanPool"): + module = parts[5:] + else: + return False + return bool(module) and any( + module[0] == name or module[0].startswith(name + ".") for name in projects + ) + + +def pack(root: Path, base: str, head: str, output: Path) -> None: + """Store only compiled PR project modules, not the whole 7 GiB pool.""" + projects = _projects(root, base, head) + manifest = { + "version": 1, + "head": head, + "projects": projects, + "sources": _source_hashes(root, projects), + "inputs": { + name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in PINNED_INPUTS + }, + } + payload = json.dumps(manifest, sort_keys=True).encode() + with tarfile.open(output, "w:gz", compresslevel=1) as archive: + entry = tarfile.TarInfo(MANIFEST) + entry.size = len(payload) + archive.addfile(entry, io.BytesIO(payload)) + for directory in ( + root / ".lake/build/ir/LeanPool", + root / ".lake/build/lib/lean/LeanPool", + ): + if directory.is_dir(): + for path in directory.rglob("*"): + relative = PurePosixPath(path.relative_to(root).as_posix()) + if path.is_file() and _build_file_for_project( + relative, set(projects) + ): + archive.add(path, arcname=relative.as_posix(), recursive=False) + + +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" + artifacts = [ + artifact + for artifact in github_json(endpoint)["artifacts"] + if artifact["name"] == ARTIFACT and not artifact["expired"] + ] + if not artifacts: + raise ValueError("prior PR build artifact unavailable") + artifact_id = max(artifacts, key=lambda artifact: artifact["id"])["id"] + with tempfile.TemporaryDirectory(prefix="lean-rebase-build-") as temporary: + zipped = Path(temporary) / "artifact.zip" + with zipped.open("wb") as output: + subprocess.run( + [ + "gh", + "api", + f"repos/{repository}/actions/artifacts/{artifact_id}/zip", + ], + stdout=output, + check=True, + timeout=600, + ) + with zipfile.ZipFile(zipped) as wrapper: + if wrapper.namelist() != [ARCHIVE]: + raise ValueError("unexpected artifact contents") + with wrapper.open(ARCHIVE) as source: + archive_path = Path(temporary) / ARCHIVE + with archive_path.open("wb") as output: + shutil.copyfileobj(source, output) + with tarfile.open(archive_path, "r:gz") as archive: + member = archive.extractfile(MANIFEST) + if member is None: + raise ValueError("missing project build manifest") + manifest = json.load(member) + projects = manifest.get("projects") + if not isinstance(projects, list) or not all( + isinstance(project, str) and PROJECT.fullmatch(project) + for project in projects + ): + raise ValueError("invalid project build manifest") + if ( + manifest.get("version") != 1 + or manifest.get("head") != previous_head + or manifest.get("sources") != _source_hashes(root, projects) + or manifest.get("inputs") + != { + name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in PINNED_INPUTS + } + ): + raise ValueError("project build inputs changed") + members = [ + member for member in archive.getmembers() if member.name != MANIFEST + ] + for entry in members: + relative = PurePosixPath(entry.name) + if ( + not entry.isfile() + or ".." in relative.parts + or not _build_file_for_project(relative, set(projects)) + ): + raise ValueError(f"unexpected project artifact: {entry.name}") + archive.extractall(root, members=members, filter="data") + + +def restore_new_main_projects( + root: Path, repository: str, previous: str, base: str +) -> None: + """Overlay merged PR artifacts before main's own large cache is published.""" + old_base = git(root, "merge-base", previous, base) + commits = git( + root, "rev-list", "--first-parent", "--reverse", f"{old_base}..{base}" + ) + for commit in commits.splitlines(): + 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 + ): + continue + try: + pulls = github_json(f"repos/{repository}/commits/{commit}/pulls") + for pull in pulls: + if not pull.get("merged_at"): + continue + head = pull["head"]["sha"] + run = _successful_run( + repository, + "lean_action_ci.yml", + pull["number"], + head, + merged=True, + ) + if run is not None and _has_build_artifact(repository, run["id"]): + restore(root, repository, run["id"], head) + print(f"Restored merged PR #{pull['number']} project build") + break + except ( + OSError, + ValueError, + KeyError, + subprocess.SubprocessError, + tarfile.TarError, + ): + print(f"No reusable project build for {commit}; Lake will build it") + + +def main() -> int: + """Run the eligibility, artifact, or generated-index command.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "command", choices=("decide", "check-index", "pack", "restore", "restore-main") + ) + parser.add_argument("--repo-root", type=Path, default=Path.cwd()) + parser.add_argument("--repository", default=os.environ.get("GITHUB_REPOSITORY", "")) + parser.add_argument("--workflow", default="lean_action_ci.yml") + parser.add_argument("--number", type=int, default=0) + parser.add_argument("--head", default="") + parser.add_argument("--base", default="") + parser.add_argument("--run-id", type=int, default=0) + parser.add_argument("--output", type=Path, default=Path(ARCHIVE)) + args = parser.parse_args() + root = args.repo_root.resolve() + if args.command == "decide": + try: + print( + json.dumps( + decision( + root, + args.repository, + args.workflow, + args.number, + args.head, + args.base, + ) + ) + ) + except (OSError, ValueError, KeyError, subprocess.SubprocessError): + print( + json.dumps( + {"eligible": False, "reason": "could not verify earlier PR run"} + ) + ) + elif args.command == "check-index": + if not check_index(root): + print("Generated LeanPool.lean is out of date", file=sys.stderr) + return 1 + elif args.command == "pack": + pack(root, args.base, args.head, args.output) + elif args.command == "restore": + restore(root, args.repository, args.run_id, args.head) + else: + restore_new_main_projects(root, args.repository, args.head, args.base) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/python/tests/test_rebase_fastpath.py b/python/tests/test_rebase_fastpath.py new file mode 100644 index 0000000000..b3a87cd3db --- /dev/null +++ b/python/tests/test_rebase_fastpath.py @@ -0,0 +1,355 @@ +"""The rebase shortcut must reject edits that need a fresh full validation.""" + +from __future__ import annotations + +import io +import json +import subprocess +import tarfile +import zipfile +from pathlib import Path + +import pytest + +from lean_pool import rebase_fastpath + + +def _git(root: Path, *arguments: str) -> str: + return subprocess.check_output(["git", *arguments], cwd=root, text=True).strip() + + +def _run(root: Path, *arguments: str) -> None: + subprocess.run(["git", *arguments], cwd=root, check=True, capture_output=True) + + +def _index(root: Path) -> None: + modules = sorted(path.stem for path in (root / "LeanPool").glob("*.lean")) + (root / "LeanPool.lean").write_text( + "module -- shake: keep-all --deprecated_module: ignore\n\n" + + "".join(f"public import LeanPool.{name}\n" for name in modules) + ) + + +def _commit(root: Path, message: str) -> str: + _run(root, "add", ".") + _run(root, "commit", "-qm", message) + return _git(root, "rev-parse", "HEAD") + + +@pytest.fixture +def rebased(tmp_path: Path) -> tuple[Path, str, str, str, str]: + """Construct a passing PR followed by a mechanical content merge of main.""" + root = tmp_path / "repo" + root.mkdir() + _run(root, "init", "-q", "-b", "main") + _run(root, "config", "user.email", "test@example.com") + _run(root, "config", "user.name", "Test") + (root / "LeanPool").mkdir() + (root / "LeanPool/A.lean").write_text("module\n") + (root / "LeanPool/projects.yml").write_text("projects:\n - slug: a\n") + for name in rebase_fastpath.PINNED_INPUTS: + (root / name).write_text(name) + _index(root) + old_base = _commit(root, "base") + + _run(root, "checkout", "-qb", "pr") + (root / "LeanPool/B.lean").write_text("module\npublic import LeanPool.A\n") + (root / "LeanPool/projects.yml").write_text("projects:\n - slug: a\n - slug: b\n") + _index(root) + previous = _commit(root, "add B") + + _run(root, "checkout", "-q", "main") + (root / "LeanPool/C.lean").write_text("module\npublic import LeanPool.A\n") + (root / "LeanPool/projects.yml").write_text("projects:\n - slug: a\n - slug: c\n") + _index(root) + base = _commit(root, "add C") + + _run(root, "checkout", "-q", "pr") + subprocess.run( + ["git", "merge", "--no-ff", "--no-commit", "main"], + cwd=root, + capture_output=True, + ) + (root / "LeanPool/projects.yml").write_text( + "projects:\n - slug: a\n - slug: c\n - slug: b\n" + ) + _index(root) + head = _commit(root, "merge main") + return root, old_base, previous, base, head + + +def _github( + monkeypatch: pytest.MonkeyPatch, previous: str, *, green: bool = True +) -> None: + def read(endpoint: str) -> dict: + if endpoint.endswith("/artifacts?per_page=100"): + return { + "artifacts": [ + {"id": 8, "name": rebase_fastpath.ARTIFACT, "expired": False} + ] + } + return { + "workflow_runs": [ + { + "id": 7, + "head_sha": previous, + "conclusion": "success" if green else "failure", + # GitHub may report the PR's current base on an old run. + "pull_requests": [{"number": 42, "base": {"sha": "f" * 40}}], + } + ] + } + + monkeypatch.setattr(rebase_fastpath, "github_json", read) + + +def test_green_content_rebase_uses_fast_path( + rebased: tuple[Path, str, str, str, str], monkeypatch: pytest.MonkeyPatch +) -> None: + """A green PR and unchanged owned module can reuse its compiled project.""" + root, _, previous, base, head = rebased + _github(monkeypatch, previous) + result = rebase_fastpath.decision( + root, "owner/repo", "lean_action_ci.yml", 42, head, base + ) + assert result == { + "eligible": True, + "reason": "verified rebase", + "run_id": 7, + "previous_head": previous, + } + assert rebase_fastpath.check_index(root) + (root / "LeanPool.lean").write_text("module\n") + assert not rebase_fastpath.check_index(root) + + +def test_missing_green_run_or_artifact_falls_back( + rebased: tuple[Path, str, str, str, str], monkeypatch: pytest.MonkeyPatch +) -> None: + """Unverified or expired evidence never bypasses Lean compilation.""" + root, _, previous, base, head = rebased + _github(monkeypatch, previous, green=False) + assert not rebase_fastpath.decision( + root, "owner/repo", "lean_action_ci.yml", 42, head, base + )["eligible"] + _github(monkeypatch, previous) + monkeypatch.setattr(rebase_fastpath, "_has_build_artifact", lambda *_: False) + assert not rebase_fastpath.decision( + root, "owner/repo", "lean_action_ci.yml", 42, head, base + )["eligible"] + assert rebase_fastpath.decision(root, "owner/repo", "docs.yml", 42, head, base)[ + "eligible" + ] + + +def test_merged_pr_run_can_have_no_pull_request_association( + monkeypatch: pytest.MonkeyPatch, +) -> None: + """GitHub removes PR associations from old runs after their PR merges.""" + head = "a" * 40 + monkeypatch.setattr( + rebase_fastpath, + "github_json", + lambda _: { + "workflow_runs": [ + { + "id": 7, + "head_sha": head, + "conclusion": "success", + "pull_requests": [], + } + ] + }, + ) + assert ( + rebase_fastpath._successful_run("owner/repo", "lean_action_ci.yml", 42, head) + is None + ) + assert rebase_fastpath._successful_run( + "owner/repo", "lean_action_ci.yml", 42, head, merged=True + ) == {"id": 7, "head_sha": head, "conclusion": "success", "pull_requests": []} + + +def test_changed_pr_project_rejected( + rebased: tuple[Path, str, str, str, str], monkeypatch: pytest.MonkeyPatch +) -> None: + """Edits to the PR's own proof require ordinary CI.""" + root, _, previous, base, _ = rebased + _github(monkeypatch, previous) + _run(root, "reset", "--hard", "HEAD^") + subprocess.run( + ["git", "merge", "--no-ff", "--no-commit", "main"], + cwd=root, + capture_output=True, + ) + (root / "LeanPool/B.lean").write_text("module\npublic import LeanPool.C\n") + (root / "LeanPool/projects.yml").write_text( + "projects:\n - slug: a\n - slug: c\n - slug: b\n" + ) + _index(root) + head = _commit(root, "merge and edit B") + assert not rebase_fastpath.decision( + root, "owner/repo", "lean_action_ci.yml", 42, head, base + )["eligible"] + + +def test_main_build_input_change_rejected( + rebased: tuple[Path, str, str, str, str], monkeypatch: pytest.MonkeyPatch +) -> None: + """A toolchain change must invalidate earlier results.""" + root, _, previous, _, _ = rebased + _github(monkeypatch, previous) + _run(root, "reset", "--hard", previous) + _run(root, "checkout", "-q", "main") + (root / "lean-toolchain").write_text("different toolchain") + base = _commit(root, "bump toolchain") + _run(root, "checkout", "-q", "pr") + subprocess.run( + ["git", "merge", "--no-ff", "--no-commit", "main"], + cwd=root, + capture_output=True, + ) + (root / "LeanPool/projects.yml").write_text( + "projects:\n - slug: a\n - slug: c\n - slug: b\n" + ) + _index(root) + head = _commit(root, "merge new main") + result = rebase_fastpath.decision( + root, "owner/repo", "lean_action_ci.yml", 42, head, base + ) + assert result["reason"] == "main changed shared build or validation inputs" + + +def test_main_edit_to_existing_lean_source_rejected( + rebased: tuple[Path, str, str, str, str], monkeypatch: pytest.MonkeyPatch +) -> None: + """A changed dependency may invalidate a previous proof or axiom audit.""" + root, _, previous, _, _ = rebased + _github(monkeypatch, previous) + _run(root, "reset", "--hard", previous) + _run(root, "checkout", "-q", "main") + (root / "LeanPool/A.lean").write_text("module\n-- changed dependency\n") + base = _commit(root, "modify A") + _run(root, "checkout", "-q", "pr") + subprocess.run( + ["git", "merge", "--no-ff", "--no-commit", "main"], + cwd=root, + capture_output=True, + ) + (root / "LeanPool/projects.yml").write_text( + "projects:\n - slug: a\n - slug: c\n - slug: b\n" + ) + _index(root) + head = _commit(root, "merge changed A") + result = rebase_fastpath.decision( + root, "owner/repo", "lean_action_ci.yml", 42, head, base + ) + assert result["reason"] == "main edited existing Lean sources" + + +def test_changed_project_card_rejected( + rebased: tuple[Path, str, str, str, str], monkeypatch: pytest.MonkeyPatch +) -> None: + """A bot merge cannot silently alter the PR's validated project card.""" + root, _, previous, base, _ = rebased + _github(monkeypatch, previous) + _run(root, "reset", "--hard", previous) + subprocess.run( + ["git", "merge", "--no-ff", "--no-commit", "main"], + cwd=root, + capture_output=True, + ) + (root / "LeanPool/projects.yml").write_text( + "projects:\n - slug: a\n - slug: c\n - slug: b-edited\n" + ) + _index(root) + head = _commit(root, "merge with changed card") + result = rebase_fastpath.decision(root, "owner/repo", "docs.yml", 42, head, base) + assert result["reason"] == "project cards changed beyond the merge" + + +def test_project_archive_contains_only_pr_module( + rebased: tuple[Path, str, str, str, str], tmp_path: Path +) -> None: + """The reusable artifact excludes the rest of the large pool build.""" + root, _, _, base, head = rebased + for project in ("A", "B", "C"): + path = root / ".lake/build/lib/lean/LeanPool" / f"{project}.olean" + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(project) + archive_path = tmp_path / "build.tar.gz" + rebase_fastpath.pack(root, base, head, archive_path) + with tarfile.open(archive_path, "r:gz") as archive: + names = archive.getnames() + manifest = json.load(archive.extractfile(rebase_fastpath.MANIFEST)) + assert manifest["projects"] == ["B"] + assert ".lake/build/lib/lean/LeanPool/B.olean" in names + assert ".lake/build/lib/lean/LeanPool/A.olean" not in names + assert ".lake/build/lib/lean/LeanPool/C.olean" not in names + + +def test_restore_checks_sources_before_overlay( + rebased: tuple[Path, str, str, str, str], + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + """A changed project cannot consume an old olean artifact.""" + root, old_base, previous, _, _ = rebased + compiled = root / ".lake/build/lib/lean/LeanPool/B.olean" + compiled.parent.mkdir(parents=True) + compiled.write_text("validated build") + archive_path = tmp_path / "build.tar.gz" + rebase_fastpath.pack(root, old_base, previous, archive_path) + compiled.unlink() + wrapper = io.BytesIO() + with zipfile.ZipFile(wrapper, "w") as zipped: + zipped.writestr(rebase_fastpath.ARCHIVE, archive_path.read_bytes()) + + monkeypatch.setattr( + rebase_fastpath, + "github_json", + lambda _: { + "artifacts": [{"id": 8, "name": rebase_fastpath.ARTIFACT, "expired": False}] + }, + ) + + def download( + command: list[str], *, stdout: io.BufferedWriter, **_kwargs: object + ) -> None: + assert command == ["gh", "api", "repos/owner/repo/actions/artifacts/8/zip"] + stdout.write(wrapper.getvalue()) + + monkeypatch.setattr(rebase_fastpath.subprocess, "run", download) + source = root / "LeanPool/B.lean" + original = source.read_text() + source.write_text("module\n-- unvalidated edit\n") + with pytest.raises(ValueError, match="project build inputs changed"): + rebase_fastpath.restore(root, "owner/repo", 7, previous) + assert not compiled.exists() + source.write_text(original) + rebase_fastpath.restore(root, "owner/repo", 7, previous) + assert compiled.read_text() == "validated build" + + +def test_new_main_project_reuses_its_merged_pr_artifact( + rebased: tuple[Path, str, str, str, str], monkeypatch: pytest.MonkeyPatch +) -> None: + """The main-cache gap need not force every waiting PR to compile the merger.""" + root, _, previous, base, _ = rebased + merged_head = "c" * 40 + restored = [] + + def read(endpoint: str) -> list[dict]: + assert endpoint == f"repos/owner/repo/commits/{base}/pulls" + return [{"number": 99, "head": {"sha": merged_head}, "merged_at": "now"}] + + monkeypatch.setattr(rebase_fastpath, "github_json", read) + monkeypatch.setattr(rebase_fastpath, "_successful_run", lambda *_, **__: {"id": 11}) + monkeypatch.setattr(rebase_fastpath, "_has_build_artifact", lambda *_: True) + monkeypatch.setattr( + rebase_fastpath, + "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)]