Restore the merge queue's build on main after a toolchain bump

.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.

.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

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,

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)]