[Vilin97]

Problem

CI runs take hours even with a "cache hit", and the merge queue has duplicate runs.

1. Stale build cache. Only one LeanPoolBuild cache exists, saved on 2026-10-16. Since then every main push run's Save pool build step failed with the runner out of disk (Free space left: 52 MB, tar exit 2). actions/cache treats that as a warning, so the runs stayed green. Every PR, merge-group and main run therefore restores the Oct 16 cache and rebuilds everything merged since. Example: merge group for Reduce Erdos97ConvexOctagon peak compiler memory #717 (one-project change) rebuilt 5,351 modules / 11.5 CPU-hours in 3h27m — mostly ConwaySoifer (190 min), Superdiffusion (174 min), HopfProblem (60 min), BrillNoetherGraphs (48 min).
2. Discarded queue runs keep building. The generated-metadata bot pushes straight to main after each merge, so GitHub rebuilds every queued group. The old groups' refs are deleted but their runs keep building for hours (3 such runs were live just now).

Changes

• Free runner disk space step (removes dotnet / Android / GHC / CodeQL / Swift, ~25 GB) in the build, shard, finalize and rebase jobs.
• Verify pool build cache step on main: fails the run if the cache key is not actually present after saving, so this cannot go silent again.
• Cancel discarded merge-group runs step in plan for merge_group events: cancels in-progress queue runs whose gh-readonly-queue/... ref returns 404 (continue-on-error, never blocks the run). plan gets actions: write for this.

Validation

• actionlint clean; test_ci_cache_contract.py, test_rebase_fastpath.py, test_ci_artifacts.py pass (122 tests).
• The 404 check was run by hand against the live queue: it found exactly the 3 discarded runs and none of the 3 current ones.
• The real proof is the first main push after merge: it should save a fresh cache, after which merge-group builds drop back to minutes.

🤖 Generated with Claude Code

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium impact] The PR appears safe to merge; both earlier findings are addressed and no new blocking issue was found.

Summary

The PR frees runner disk space, checks that main build caches were saved, and cancels discarded merge-queue runs.

• Main Lean builds clear runner space and verify their saved cache.
• The merge queue cancels runs whose refs have been discarded.

_{Reviews (3) · Last reviewed commit: "Leave build-cache pruning to the schedul..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "Post-merge review of published commit abb701f across all three changed files. The earlier shell-404 and inline-pruning findings are addressed. A remaining per-run timeout aborts the cleanup sweep; an offline mocked execution reproduced it. The focused Python-only repair is prepared in draft PR736, where all nine targeted tests and Ruff checks pass.",
"assessment": {
"scope": "CI cache health and discarded-run cleanup",
"risk": "medium",
"repair_status": "Draft PR736 isolates lookup and cancellation failures and reports only accepted cancellation requests.",
"integration": "Current-main qualification, all normal checks and the standing workflow authority conditions remain independent."
},
"verdict": "request_changes",
"findings": [
{
"priority": "P2",
"file": "python/lean_pool/merge_queue_cleanup.py",
"line": 39,
"rule": "isolate-best-effort-cleanup-failures",
"comment": "A ref lookup TimeoutExpired escapes branch_exists and aborts discarded_runs before later definite-404 runs are checked; even IDs selected before that timeout never reach the cancellation loop. A timeout in the cancellation loop at line84 likewise stops later requests. continue-on-error preserves the workflow but cannot resume the sweep. Catch lookup timeouts as unknown/keep and isolate cancellation errors per run, with timeout-followed-by-another-run regression coverage. Draft PR736 contains this repair."
}
],
"follow_up": "#736"
}