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. diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 8990a93522..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 @@ -199,6 +200,16 @@ 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. + 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 @@ -301,8 +312,30 @@ jobs: exit 1 fi + - name: Restore the merge queue's full build + id: queue-full-build + if: needs.plan.outputs.queue_build == 'true' && 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" + + # 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' + 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 +388,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 +403,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 +777,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 +792,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..19d166d73a 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -716,3 +716,54 @@ 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" + ) + 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"]