From 67162a7602d132a2776bd84074acd44ec593fc95 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 3 Nov 2026 08:51:25 -0800 Subject: [PATCH 1/3] Restore the merge queue's build on main after a toolchain bump Main cannot read caches saved by merge-queue runs. After a Lean/Mathlib bump (or a cache eviction) the push run therefore found no build cache and rebuilt the whole pool in shards: 4.5h after #530, while PRs ran cold too. A merge-queue build that starts cold now also uploads its full build as the existing lean-pool-build artifact. When the main push run is cold, the planner checks whether the green queue run for that exact commit published one; if so it plans a single job that restores it, verifies the tree and pins, replays Lake, and saves main's cache. Any miss falls back to the ordinary build. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean_action_ci.yml | 29 ++++++-- python/lean_pool/ci_artifacts.py | 86 +++++++++++++++++----- python/tests/test_ci_artifacts.py | 99 ++++++++++++++++++++++++++ python/tests/test_ci_cache_contract.py | 36 ++++++++++ 4 files changed, 227 insertions(+), 23 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 8990a93522..9447f25f31 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -199,6 +199,13 @@ jobs: plan=$(CHANGED_FILES_PATH="$changed_files" DIFF_AVAILABLE="$diff_available" \ COLD="$cold" FORCE_FULL="$FORCE_FULL" \ python3 scripts/ci/plan-build-shards.py) + # Main cannot read merge-queue caches, so after a toolchain bump it + # would rebuild the whole pool again; restore the queue's build instead. + if [ "$EVENT_NAME" = push ] && [ "$cold" = true ] && [ "$FORCE_FULL" != true ] \ + && PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore-queue \ + --repository "$REPOSITORY" --head "$GITHUB_SHA" --check; then + plan='{"mode":"single","matrix":{"include":[{"shard":"00","projects":""}]}}' + fi reuse_run_id="" previous_head="" if [ "$EVENT_NAME" = "pull_request" ] && [ "$FORCE_FULL" != "true" ] && [ "$minimal_build" != true ]; then @@ -301,8 +308,18 @@ jobs: exit 1 fi + - name: Restore the merge queue's full build + id: queue-full-build + if: github.event_name == 'push' && steps.cache.outputs.cache-matched-key == '' + continue-on-error: true + env: + GH_TOKEN: ${{ github.token }} + run: >- + PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore-queue + --head "$GITHUB_SHA" + - name: Reuse compiled projects from merged PRs - if: github.event_name == 'push' && steps.cache.outputs.cache-hit != 'true' + if: github.event_name == 'push' && steps.cache.outputs.cache-hit != 'true' && steps.queue-full-build.outcome != 'success' continue-on-error: true env: GH_TOKEN: ${{ github.token }} @@ -355,8 +372,9 @@ jobs: # Main publishes the shared full build. A minimal-verifier PR publishes # only its own projects; the verifier overlays them on the main cache. + # A cold merge-queue build publishes it too, for main to restore. - name: Package build for documentation - if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') + if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') || (github.event_name == 'merge_group' && steps.cache.outputs.cache-matched-key == '') env: BUILD_EVENT: ${{ github.event_name }} BASE_SHA: ${{ github.event.pull_request.base.sha }} @@ -369,7 +387,7 @@ jobs: fi - name: Share build with documentation - if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') + if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') || (github.event_name == 'merge_group' && steps.cache.outputs.cache-matched-key == '') uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 with: name: lean-pool-build @@ -743,8 +761,9 @@ jobs: # Main publishes the shared full build. A minimal-verifier PR publishes # only its own projects; the verifier overlays them on the main cache. + # A cold merge-queue build publishes it too, for main to restore. - name: Package build for documentation - if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') + if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') || (github.event_name == 'merge_group' && steps.cache.outputs.cache-matched-key == '') env: BUILD_EVENT: ${{ github.event_name }} BASE_SHA: ${{ github.event.pull_request.base.sha }} @@ -757,7 +776,7 @@ jobs: fi - name: Share build with documentation - if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') + if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') || (github.event_name == 'merge_group' && steps.cache.outputs.cache-matched-key == '') uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 with: name: lean-pool-build diff --git a/python/lean_pool/ci_artifacts.py b/python/lean_pool/ci_artifacts.py index f4c2e884d7..79eca76424 100644 --- a/python/lean_pool/ci_artifacts.py +++ b/python/lean_pool/ci_artifacts.py @@ -5,7 +5,8 @@ normal build traces afterwards. Missing or incompatible artifacts fall back to the ordinary Lake build. PR overlays preserve the shared main cache and contain only projects changed in the author's diff, including a manifest-only archive -for infrastructure changes. +for infrastructure changes. A cold merge-queue build also publishes its full +build, which main restores instead of rebuilding after a toolchain bump. """ from __future__ import annotations @@ -38,6 +39,15 @@ LEGACY_ARCHIVE_NAME = "lean-pool-build.tar.gz" MANIFEST_NAME = "build-manifest.json" PROJECT = re.compile(r"[A-Za-z][A-Za-z0-9_]*\Z") +RECOVERY_ERRORS = ( + subprocess.SubprocessError, + OSError, + ValueError, + KeyError, + tarfile.TarError, + EOFError, + zipfile.BadZipFile, +) def _project_output(path: PurePosixPath, projects: list[str]) -> bool: @@ -283,19 +293,55 @@ def matching_run(repository: str, head: str, event: str) -> dict | None: return max(runs, key=lambda run: run["id"]) if runs else None +def published_artifact(repository: str, run_id: int) -> int | None: + """Return the newest unexpired build archive a run has uploaded.""" + endpoint = f"repos/{repository}/actions/runs/{run_id}/artifacts?per_page=100" + matches = [ + artifact["id"] + for artifact in github_json(endpoint)["artifacts"] + if artifact["name"] == ARTIFACT_NAME and not artifact["expired"] + ] + return max(matches, default=None) + + +def queue_build_artifact(repository: str, head: str) -> int | None: + """Find the full build a green merge-queue run published for this commit. + + Main's caches cannot read merge-queue caches, so after a toolchain bump or + cache eviction this archive is main's only alternative to a cold rebuild. + """ + run = matching_run(repository, head, "merge_group") + if run is None or run.get("conclusion") != "success": + return None + return published_artifact(repository, run["id"]) + + +def reuse_queue_build( + root: Path, repository: str, head: str, *, check_only: bool = False +) -> bool: + """Install the merged queue's full build; any miss falls back to Lake.""" + try: + artifact = queue_build_artifact(repository, head) + if artifact is None: + LOGGER.info("The merge queue published no full build for %s", head) + return False + if check_only: + LOGGER.info("The merge queue published a full build for %s", head) + return True + return download_build(root, repository, artifact) + except RECOVERY_ERRORS: + LOGGER.exception("Could not reuse the merge queue build; using Lake") + return False + + def wait_for_artifact(repository: str, run: dict, wait_seconds: int) -> int | None: """Wait for compiled output without waiting for later lint/quality stages.""" deadline = time.monotonic() + wait_seconds endpoint = f"repos/{repository}/actions/runs/{run['id']}" while True: - artifacts = github_json(f"{endpoint}/artifacts?per_page=100")["artifacts"] - matches = [ - artifact - for artifact in artifacts - if artifact["name"] == ARTIFACT_NAME and not artifact["expired"] - ] - if matches: - return max(matches, key=lambda artifact: artifact["id"])["id"] + artifact = published_artifact(repository, run["id"]) + if artifact is not None: + return artifact status = github_json(endpoint) if status["status"] == "completed" or time.monotonic() >= deadline: return None @@ -403,15 +449,7 @@ def reuse_build( ) return False return download_build(root, repository, artifact) - except ( - subprocess.SubprocessError, - OSError, - ValueError, - KeyError, - tarfile.TarError, - EOFError, - zipfile.BadZipFile, - ): + except RECOVERY_ERRORS: LOGGER.exception("Could not reuse CI output; using the regular Lake build") return False @@ -434,12 +472,24 @@ def main() -> None: command.add_argument("--event", required=True) command.add_argument("--wait-seconds", type=int, default=7200) restore.add_argument("--pull-request-artifact", action="store_true") + queue = commands.add_parser("restore-queue") + queue.add_argument("--repository", default=os.environ.get("GITHUB_REPOSITORY")) + queue.add_argument("--head", required=True) + queue.add_argument("--check", action="store_true") arguments = parser.parse_args() logging.basicConfig(level=logging.INFO, format="ci-artifacts: %(message)s") if arguments.command == "pack": pack_build( Path.cwd(), arguments.output, base=arguments.base, head=arguments.head ) + elif arguments.command == "restore-queue": + restored = reuse_queue_build( + Path.cwd(), + arguments.repository, + arguments.head, + check_only=arguments.check, + ) + raise SystemExit(0 if restored else 1) elif arguments.command == "wait": wait_for_build( arguments.repository, diff --git a/python/tests/test_ci_artifacts.py b/python/tests/test_ci_artifacts.py index 12ef5ec035..f42bd2c440 100644 --- a/python/tests/test_ci_artifacts.py +++ b/python/tests/test_ci_artifacts.py @@ -557,3 +557,102 @@ def test_project_overlay_rejects_unowned_outputs_before_install(repository): assert ( repository / ".lake/build/lib/lean/LeanPool.olean" ).read_bytes() == b"compiled" + + +def _queue_responses(conclusion: str, artifacts: list[dict]): + def response(endpoint): + if "/artifacts?" in endpoint: + assert endpoint.startswith("repos/owner/repo/actions/runs/9/artifacts?") + return {"artifacts": artifacts} + assert "head_sha=abc123&event=merge_group&" in endpoint + return { + "workflow_runs": [ + {"id": 3, "conclusion": "success"}, + {"id": 9, "conclusion": conclusion}, + ] + } + + return response + + +def test_queue_build_uses_latest_green_exact_head_run(monkeypatch) -> None: + """Main restores only an unexpired full build from the merged queue attempt.""" + artifacts = [ + {"id": 4, "name": "lean-pool-build", "expired": False}, + {"id": 6, "name": "lean-pool-build", "expired": True}, + {"id": 8, "name": "rebase-project-build", "expired": False}, + ] + monkeypatch.setattr( + ci_artifacts, "github_json", _queue_responses("success", artifacts) + ) + assert ci_artifacts.queue_build_artifact("owner/repo", "abc123") == 4 + + +def test_queue_build_ignores_failed_latest_attempt(monkeypatch) -> None: + """A newer failed attempt is never hidden by an older green one.""" + artifacts = [{"id": 4, "name": "lean-pool-build", "expired": False}] + monkeypatch.setattr( + ci_artifacts, "github_json", _queue_responses("failure", artifacts) + ) + assert ci_artifacts.queue_build_artifact("owner/repo", "abc123") is None + + +def test_queue_build_check_does_not_download(repository: Path, monkeypatch) -> None: + """The planner only asks whether the archive exists; the build job installs it.""" + monkeypatch.setattr(ci_artifacts, "queue_build_artifact", lambda *args: 4) + + def unexpected(*args): + pytest.fail("checking must not download the build") + + monkeypatch.setattr(ci_artifacts, "download_build", unexpected) + assert ci_artifacts.reuse_queue_build( + repository, "owner/repo", "abc123", check_only=True + ) + + +def test_queue_build_restore_installs_artifact(repository: Path, monkeypatch) -> None: + """The build job installs the queue's archive through the verified download.""" + downloads = [] + monkeypatch.setattr(ci_artifacts, "queue_build_artifact", lambda *args: 4) + monkeypatch.setattr( + ci_artifacts, + "download_build", + lambda root, repository, artifact: downloads.append(artifact) or True, + ) + assert ci_artifacts.reuse_queue_build(repository, "owner/repo", "abc123") + assert downloads == [4] + + +@pytest.mark.parametrize("failure", [None, subprocess.CalledProcessError(1, "gh")]) +def test_queue_build_miss_falls_back(repository: Path, monkeypatch, failure) -> None: + """A missing archive or API error leaves the ordinary build path in place.""" + + def lookup(*args): + if failure is not None: + raise failure + + monkeypatch.setattr(ci_artifacts, "queue_build_artifact", lookup) + assert not ci_artifacts.reuse_queue_build( + repository, "owner/repo", "abc123", check_only=True + ) + + +@pytest.mark.parametrize("restored", [True, False]) +def test_restore_queue_command_reports_outcome(monkeypatch, restored: bool) -> None: + """The planner and build job branch on the command's exit status.""" + calls = [] + + def reuse(root, repository, head, *, check_only): + calls.append((repository, head, check_only)) + return restored + + monkeypatch.setattr(ci_artifacts, "reuse_queue_build", reuse) + monkeypatch.setattr( + sys, + "argv", + ["ci_artifacts", "restore-queue", "--repository", "o/r", "--head", "h"], + ) + with pytest.raises(SystemExit) as exit_info: + ci_artifacts.main() + assert exit_info.value.code == (0 if restored else 1) + assert calls == [("o/r", "h", False)] diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index cbfd2c2956..28e51ce4be 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -716,3 +716,39 @@ def test_profiling_is_automatic_and_cache_pruning_is_scheduled() -> None: for job in workflow["jobs"].values() for step in job["steps"] ) + + +def test_cold_main_push_restores_the_merged_queue_build() -> None: + """Cold queue builds publish the full archive that a cold main push restores.""" + workflow = (WORKFLOWS / "lean_action_ci.yml").read_text() + jobs = yaml.safe_load(workflow)["jobs"] + for name in ("build", "finalize"): + steps = {step.get("name"): step for step in jobs[name]["steps"]} + for producer in ( + "Package build for documentation", + "Share build with documentation", + ): + condition = steps[producer]["if"] + assert ( + "github.event_name == 'merge_group' && " + "steps.cache.outputs.cache-matched-key == ''" + ) in condition + plan = next( + step for step in jobs["plan"]["steps"] if step.get("name") == "Plan the build" + ) + assert "ci_artifacts restore-queue" in plan["run"] + assert '--check; then\n plan=\'{"mode":"single"' in plan["run"] + steps = jobs["build"]["steps"] + names = [step.get("name") for step in steps] + restore = steps[names.index("Restore the merge queue's full build")] + assert restore["continue-on-error"] is True + assert "ci_artifacts restore-queue" in restore["run"] + assert "--check" not in restore["run"] + assert names.index("Restore pool build") < names.index( + "Restore the merge queue's full build" + ) + assert names.index("Restore the merge queue's full build") < names.index( + "Build project" + ) + overlay = steps[names.index("Reuse compiled projects from merged PRs")] + assert "steps.queue-full-build.outcome != 'success'" in overlay["if"] From 88f424351c65dbbcfbe3b615a169db96d736ed89 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 3 Nov 2026 08:58:02 -0800 Subject: [PATCH 2/3] Fall back to a sharded rebuild when the queue build cannot be restored The planner trades the sharded plan for the restore, so a failed download would leave one job compiling the whole pool. Record the planner's choice as an output and, if the restore fails, dispatch a force_full sharded run and stop this job. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean_action_ci.yml | 18 +++++++++++++++++- python/tests/test_ci_cache_contract.py | 15 +++++++++++++++ 2 files changed, 32 insertions(+), 1 deletion(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 9447f25f31..946ebe09f5 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -95,6 +95,7 @@ jobs: matrix: ${{ steps.plan.outputs.matrix }} reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }} previous_head: ${{ steps.plan.outputs.previous_head }} + queue_build: ${{ steps.plan.outputs.queue_build }} steps: - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd @@ -201,11 +202,14 @@ jobs: python3 scripts/ci/plan-build-shards.py) # Main cannot read merge-queue caches, so after a toolchain bump it # would rebuild the whole pool again; restore the queue's build instead. + queue_build=false if [ "$EVENT_NAME" = push ] && [ "$cold" = true ] && [ "$FORCE_FULL" != true ] \ && PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore-queue \ --repository "$REPOSITORY" --head "$GITHUB_SHA" --check; then plan='{"mode":"single","matrix":{"include":[{"shard":"00","projects":""}]}}' + queue_build=true fi + echo "queue_build=$queue_build" >> "$GITHUB_OUTPUT" reuse_run_id="" previous_head="" if [ "$EVENT_NAME" = "pull_request" ] && [ "$FORCE_FULL" != "true" ] && [ "$minimal_build" != true ]; then @@ -310,7 +314,7 @@ jobs: - name: Restore the merge queue's full build id: queue-full-build - if: github.event_name == 'push' && steps.cache.outputs.cache-matched-key == '' + if: needs.plan.outputs.queue_build == 'true' && steps.cache.outputs.cache-matched-key == '' continue-on-error: true env: GH_TOKEN: ${{ github.token }} @@ -318,6 +322,18 @@ jobs: PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore-queue --head "$GITHUB_SHA" + # The planner gave up the sharded plan for this restore; one job cannot + # rebuild the whole pool in time, so hand off to a sharded full rebuild. + - name: Rebuild in shards when the queue build is unavailable + if: steps.queue-full-build.outcome == 'failure' + env: + GH_TOKEN: ${{ github.token }} + run: | + gh workflow run lean_action_ci.yml --repo "$GITHUB_REPOSITORY" \ + --ref "$GITHUB_REF_NAME" -f force_full=true + echo "::error::Could not restore the merge queue's build; started a sharded full rebuild instead." + exit 1 + - name: Reuse compiled projects from merged PRs if: github.event_name == 'push' && steps.cache.outputs.cache-hit != 'true' && steps.queue-full-build.outcome != 'success' continue-on-error: true diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 28e51ce4be..19d166d73a 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -750,5 +750,20 @@ def test_cold_main_push_restores_the_merged_queue_build() -> None: assert names.index("Restore the merge queue's full build") < names.index( "Build project" ) + assert "needs.plan.outputs.queue_build == 'true'" in restore["if"] + assert "queue_build=true" in plan["run"] + assert jobs["plan"]["outputs"]["queue_build"] + fallback = steps[ + names.index("Rebuild in shards when the queue build is unavailable") + ] + assert fallback["if"] == "steps.queue-full-build.outcome == 'failure'" + assert "-f force_full=true" in fallback["run"] + assert "exit 1" in fallback["run"] + assert names.index("Restore the merge queue's full build") < names.index( + "Rebuild in shards when the queue build is unavailable" + ) + assert names.index( + "Rebuild in shards when the queue build is unavailable" + ) < names.index("Build project") overlay = steps[names.index("Reuse compiled projects from merged PRs")] assert "steps.queue-full-build.outcome != 'success'" in overlay["if"] From 42edf1ef186a1cf09efc04622476545f679bbf44 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 5 Nov 2026 12:57:51 -0800 Subject: [PATCH 3/3] Free runner disk before Exposition Verify restores the pool build The dependency and pool build caches no longer fit in the runner's default free space, so the verify job died with ENOSPC while restoring them in the merge queue. Lean Action CI already frees the same paths. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/exposition-verify.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.github/workflows/exposition-verify.yml b/.github/workflows/exposition-verify.yml index 3c48b4bc07..432829f523 100644 --- a/.github/workflows/exposition-verify.yml +++ b/.github/workflows/exposition-verify.yml @@ -101,6 +101,14 @@ jobs: id: build-identity run: echo "revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)" >> "$GITHUB_OUTPUT" + # The dependency and pool build caches together exceed the runner's + # default free space, so restoring them fails with ENOSPC. + - name: Free runner disk space + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ + /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift + df -h / + # Match Lean Action CI's cache lookup exactly. This workflow only needs # compiled Lean artifacts; restoring doc-gen output here used to make a # broad fallback pull an incompatible cache after every toolchain bump.