Fix silent main build-cache save failures and cancel discarded queue runs

.github/workflows/lean_action_ci.yml

@@ -83,6 +83,9 @@ jobs:
   plan:
     runs-on: ubuntu-latest
     name: Plan build
+    permissions:
+      contents: read
+      actions: write
     outputs:
       build_revision: ${{ steps.build-identity.outputs.revision }}
       base_build_revision: ${{ steps.build-identity.outputs.base_revision }}
@@ -98,6 +101,19 @@ jobs:
         with:
           fetch-depth: 0
 
+      # A push to main outside the queue (such as the generated-metadata
+      # commit) makes GitHub rebuild every queued group, but the discarded
+      # groups' runs keep building for hours. Their refs are deleted, so
+      # cancel any queue run whose ref no longer exists.
+      - name: Cancel discarded merge-group runs
+        if: github.event_name == 'merge_group'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.merge_queue_cleanup
+          --repository "$GITHUB_REPOSITORY" --current-run-id "$GITHUB_RUN_ID"
+
       - name: Install Python tooling runtime
         uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
         with:
@@ -220,6 +236,15 @@ jobs:
         with:
           fetch-depth: 0
 
+      # Restored caches plus the cache-save archive overflow the runner's
+      # default free space: every main build-cache save failed from
+      # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache.
+      - 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 /
+
       # Keep the large toolchain/Mathlib cache independent of per-commit builds.
       - name: Restore Lean dependencies
         id: dependency-cache
@@ -449,12 +474,28 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Save pool build
+        id: save-build
         if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
         uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
           key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
 
+      # actions/cache only warns when a save fails; a missing main cache makes
+      # every later run rebuild from an older one, so fail loudly instead.
+      - name: Verify pool build cache
+        if: always() && steps.save-build.outcome == 'success'
+        env:
+          GH_TOKEN: ${{ github.token }}
+          KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
+        run: |
+          set -euo pipefail
+          saved=$(gh cache list --repo "$GITHUB_REPOSITORY" --key "$KEY" --json key --jq length)
+          if [ "$saved" = 0 ]; then
+            echo "::error::Pool build cache $KEY was not saved; later runs will rebuild from a stale cache."
+            exit 1
+          fi
+
   shard:
     needs: plan
     if: needs.plan.outputs.mode == 'sharded'
@@ -473,6 +514,15 @@ jobs:
         with:
           fetch-depth: 0
 
+      # Restored caches plus the cache-save archive overflow the runner's
+      # default free space: every main build-cache save failed from
+      # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache.
+      - 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 /
+
       - name: Restore Lean dependencies
         id: dependency-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
@@ -571,6 +621,15 @@ jobs:
         with:
           fetch-depth: 0
 
+      # Restored caches plus the cache-save archive overflow the runner's
+      # default free space: every main build-cache save failed from
+      # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache.
+      - 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 /
+
       - name: Restore Lean dependencies
         id: dependency-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
@@ -803,12 +862,28 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Save pool build
+        id: save-build
         if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
         uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
           key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
 
+      # actions/cache only warns when a save fails; a missing main cache makes
+      # every later run rebuild from an older one, so fail loudly instead.
+      - name: Verify pool build cache
+        if: always() && steps.save-build.outcome == 'success'
+        env:
+          GH_TOKEN: ${{ github.token }}
+          KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
+        run: |
+          set -euo pipefail
+          saved=$(gh cache list --repo "$GITHUB_REPOSITORY" --key "$KEY" --json key --jq length)
+          if [ "$saved" = 0 ]; then
+            echo "::error::Pool build cache $KEY was not saved; later runs will rebuild from a stale cache."
+            exit 1
+          fi
+
   # 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:
@@ -822,6 +897,15 @@ jobs:
         with:
           fetch-depth: 0
 
+      # Restored caches plus the cache-save archive overflow the runner's
+      # default free space: every main build-cache save failed from
+      # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache.
+      - 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 /
+
       - name: Restore Lean dependencies
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:

python/lean_pool/merge_queue_cleanup.py

@@ -0,0 +1,105 @@
+"""Cancel merge-queue CI runs whose queue entry GitHub has already discarded.
+
+A push to main from outside the queue makes GitHub rebuild every queued group
+and delete the old groups' `gh-readonly-queue/...` refs, but runs started for
+those refs keep building. A run whose ref no longer exists can never merge.
+"""
+
+from __future__ import annotations
+
+import argparse
+import json
+import logging
+import subprocess
+from collections.abc import Callable
+from typing import Any
+
+LOGGER = logging.getLogger(__name__)
+WORKFLOW = "lean_action_ci.yml"
+
+
+def discarded_runs(
+    runs: list[dict[str, Any]],
+    current_run_id: int,
+    branch_exists: Callable[[str], bool],
+) -> list[int]:
+    """Select unfinished queue runs, other than this one, whose branch is gone."""
+    return [
+        run["databaseId"]
+        for run in runs
+        if run.get("status") != "completed"
+        and run.get("databaseId") != current_run_id
+        and str(run.get("headBranch", "")).startswith("gh-readonly-queue/")
+        and not branch_exists(run["headBranch"])
+    ]
+
+
+def branch_exists(repository: str, branch: str) -> bool:
+    """Report a branch as missing only on a definite 404, never on other errors."""
+    result = subprocess.run(
+        ["gh", "api", f"repos/{repository}/git/ref/heads/{branch}"],
+        capture_output=True,
+        text=True,
+        timeout=60,
+    )
+    if result.returncode == 0:
+        return True
+    if "HTTP 404" in result.stderr:
+        return False
+    LOGGER.warning("Could not look up %s: %s", branch, result.stderr.strip())
+    return True
+
+
+def queue_runs(repository: str) -> list[dict[str, Any]]:
+    """List recent merge-group runs of the Lean CI workflow."""
+    output = subprocess.check_output(
+        [
+            "gh",
+            "run",
+            "list",
+            "--repo",
+            repository,
+            "--workflow",
+            WORKFLOW,
+            "--event",
+            "merge_group",
+            "--limit",
+            "100",
+            "--json",
+            "databaseId,status,headBranch",
+        ],
+        text=True,
+        timeout=60,
+    )
+    return json.loads(output)
+
+
+def cancel_discarded(repository: str, current_run_id: int) -> list[int]:
+    """Cancel every discarded queue run and return the cancelled run IDs."""
+    cancelled = discarded_runs(
+        queue_runs(repository),
+        current_run_id,
+        lambda branch: branch_exists(repository, branch),
+    )
+    for run_id in cancelled:
+        LOGGER.info("Cancelling run %s: its merge group was discarded", run_id)
+        subprocess.run(
+            ["gh", "run", "cancel", str(run_id), "--repo", repository],
+            check=False,
+            timeout=60,
+        )
+    return cancelled
+
+
+def main() -> None:
+    """Cancel discarded merge-group runs for one repository."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--repository", required=True)
+    parser.add_argument("--current-run-id", type=int, required=True)
+    arguments = parser.parse_args()
+    logging.basicConfig(level=logging.INFO, format="queue: %(message)s")
+    cancel_discarded(arguments.repository, arguments.current_run_id)
+
+
+if __name__ == "__main__":
+    main()

python/tests/test_merge_queue_cleanup.py

@@ -0,0 +1,84 @@
+"""Check that only runs for discarded merge groups are cancelled."""
+
+from __future__ import annotations
+
+import subprocess
+from typing import Any
+
+import pytest
+
+from lean_pool import merge_queue_cleanup
+from lean_pool.merge_queue_cleanup import (
+    branch_exists,
+    cancel_discarded,
+    discarded_runs,
+)
+
+LIVE = "gh-readonly-queue/main/pr-2-live"
+GONE = "gh-readonly-queue/main/pr-1-gone"
+ALSO_GONE = "gh-readonly-queue/main/pr-3-gone"
+
+
+def _run(identifier: int, branch: str, status: str = "in_progress") -> dict[str, Any]:
+    return {"databaseId": identifier, "headBranch": branch, "status": status}
+
+
+def test_every_missing_branch_is_selected_after_the_first() -> None:
+    """A missing ref must not stop the scan before later discarded runs."""
+    runs = [_run(1, GONE), _run(2, LIVE), _run(3, ALSO_GONE)]
+    assert discarded_runs(runs, 99, lambda branch: branch == LIVE) == [1, 3]
+
+
+def test_current_completed_and_non_queue_runs_are_kept() -> None:
+    """Never cancel this run, finished runs, or runs outside the queue."""
+    runs = [
+        _run(1, GONE),
+        _run(2, GONE, status="completed"),
+        _run(3, "feature/branch"),
+    ]
+    assert discarded_runs(runs, 1, lambda branch: False) == []
+
+
+@pytest.mark.parametrize(
+    ("returncode", "stderr", "expected"),
+    [
+        (0, "", True),
+        (1, "gh: Not Found (HTTP 404)", False),
+        (1, "gh: Server Error (HTTP 502)", True),
+    ],
+)
+def test_only_a_definite_404_counts_as_missing(
+    monkeypatch: pytest.MonkeyPatch, returncode: int, stderr: str, expected: bool
+) -> None:
+    """Transient API errors must not cancel a live queue run."""
+
+    def fake_run(*args: Any, **kwargs: Any) -> subprocess.CompletedProcess[str]:
+        return subprocess.CompletedProcess(args, returncode, "", stderr)
+
+    monkeypatch.setattr(subprocess, "run", fake_run)
+    assert branch_exists("owner/repository", GONE) is expected
+
+
+def test_cancel_discarded_cancels_each_missing_run(
+    monkeypatch: pytest.MonkeyPatch,
+) -> None:
+    """Both discarded runs are cancelled even though the first lookup 404s."""
+    cancelled: list[list[str]] = []
+    monkeypatch.setattr(
+        merge_queue_cleanup,
+        "queue_runs",
+        lambda repository: [_run(1, GONE), _run(2, LIVE), _run(3, ALSO_GONE)],
+    )
+
+    def fake_run(command: list[str], **kwargs: Any) -> subprocess.CompletedProcess[str]:
+        if command[:2] == ["gh", "api"]:
+            missing = command[2].endswith(("-gone",))
+            return subprocess.CompletedProcess(
+                command, 1 if missing else 0, "", "HTTP 404" if missing else ""
+            )
+        cancelled.append(command)
+        return subprocess.CompletedProcess(command, 0, "", "")
+
+    monkeypatch.setattr(subprocess, "run", fake_run)
+    assert cancel_discarded("owner/repository", 99) == [1, 3]
+    assert [command[3] for command in cancelled] == ["1", "3"]