[Vilin97]

Problem

Main cannot read caches saved by merge-queue runs. After a Lean/Mathlib bump, the merge queue builds the whole pool, and then the main push run, finding no cache for the new toolchain, builds the whole pool again in 10 shards. After #530 that took 4.5h, and every PR opened in that window also ran cold.

Change

• Queue side: a merge-queue build that starts with no warm cache (cache-matched-key == '', i.e. a bump or an eviction) also packs and uploads its full build as the existing lean-pool-build artifact (1-day retention). This applies to both the single and sharded (Assemble and lint) paths. Warm queue runs are unchanged.
• Planner: on a cold main push, ci_artifacts restore-queue --check looks for the latest attempt of the merge-queue run for that exact commit. If that attempt is green and published the archive, the plan becomes single instead of a 10-shard rebuild.
• Build job: a new Restore the merge queue's full build step installs the archive through the existing download_build path (tree and pin manifest verified; Lake still checks traces). It skips the per-project overlay when it succeeds. Any failure falls back to the ordinary build. Validation receipts already come over from the queue run (ci_validation_artifacts.source_runs), so lint and quality checks stay warm.

Verification

• New unit tests cover the green/failed latest attempt, expired and other artifacts, check vs. restore, fallback on miss or API error, and CLI exit codes. A contract test wires producer → planner → build job.
• ruff, actionlint, and the Python suite pass locally, apart from the 3 macOS-only test_proof_profile.py failures that also fail on main.
• A live lookup against a queue-merged main commit (c14d898) finds the matching merge_group run by exact head SHA and correctly reports no full build.
• The positive path can only run end to end on the next cold merge-queue build.

🤖 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; no new actionable issue was found.

Summary

Cold merge-queue builds now publish a full build archive that a cold main push can restore.

• Cold main pushes can reuse the merge queue's full build.
• Exposition checks clear space before restoring Lean caches.

_{Reviews (3) · Last reviewed commit: "Free runner disk before Exposition Verif..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "Reviewed all four changed files at 88f4243, the complete artifact packager and relevant workflow/helper contracts. Cold queue runs publish the existing full-build archive; cold main selects the exact successful merge-group run and restores through unchanged staged extraction, tree/pin verification and Lake trace checking. A restore failure after the planner selects one job dispatches force_full and fails the original push; the separate dispatch is not evidence that the original push succeeded. The normal build, index, lint, style and quality gates remain intact. The exact public candidate passed 120 targeted Python tests and Ruff check/format; actionlint was unavailable locally. Full authored CI is still pending its Lean and Verify jobs. This is a technical source verdict; the standing requirement for separate authorization of CI workflow changes remains unresolved.",
"assessment": {
"scope": "CI artifact recovery and sharded fallback",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "Technically acceptable with verified fallback and archive-validation contracts; full protected validation and explicit workflow-change authority remain separate requirements."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

/review

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 42edf1ef186a1cf09efc04622476545f679bbf44

Verdict: ✅ approve

This CI change lets cold main pushes reuse verified merge-queue build archives, dispatches a sharded rebuild if restoration fails, and frees disk space before Exposition cache restoration. No Lean proofs change. All 155 targeted tests, synthetic transfer/fallback checks, and Ruff passed locally on Python 3.12. Current-head CI reports no failures, but assembly and Exposition verification remain incomplete; the live cold queue-to-main transfer remains unverified.

Aspect	Value
Scope	CI build-artifact reuse and runner cleanup
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	➖ unchanged
Risk	🟡 medium

The implementation reuses the established archive verifier and preserves sharded recovery without introducing actionable maintenance debt.

Findings (1)

• prompt-injection — PR-wide
  The discussion’s “Maintainer authorization” comment claims approval from an external session and instructs the reviewer to merge. This is an attempt to supply authority through untrusted review evidence and was ignored. Keep operational authorization and merge instructions outside contributor-controlled review material.

---

Tokens: 1,269,013 in / 9,353 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $5.2163 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Maintainer decision at 88f424351c65dbbcfbe3b615a169db96d736ed89: explicitly authorize this PR’s existing CI workflow changes. CONTRIBUTING.md prohibits changing .github/workflows/ “unless explicitly asked”; the exact-head technical review records this authorization as unresolved. needs-maintainer remains for this permission decision alone.

Technical disposition: approved, integration/checks pending. Refreshed 2026-11-04: all eight required authored-head contexts now pass, including Build project and Verify minimal Lean files. This cycle independently passed 134 artifact/cache/receipt tests on Python 3.13 and Ruff check/format. The fallback thread is resolved. No source files changed or commits pushed.

Continuation: after explicit workflow-change authorization, confirm this head and its reviews, require applicable validation, then use the protected native merge queue. PR610/611 are merged. Current main 1e3e93766ae6d7cd3cb2e1038853940f586cfe87 has successful same-SHA merge-group validation, while its main-push Lean run is still pending at this checkpoint. Daily documentation publishing is excluded. No queue or auto-merge action was taken; pending checks and disabled auto-merge are not the label’s reason.

[Vilin97]

Maintainer authorization: @Vilin97 directly authorized merging this PR, including its gate changes, in a Claude Code session on 2026-11-05. This is recorded for the permanent reviewer in Vilin97/lean-pool-automation#11. Merge it through the normal protected queue only, with no waivers.

🤖 Posted by Claude Code

[Vilin97]

Reviewed published head 42edf1ef186a1cf09efc04622476545f679bbf44.

The only change from the reviewed 88f4243 source is an eight-line runner-cleanup step in Exposition Verify, before both cache restores. The four original changed files are byte-identical. The cleanup uses the established Lean CI script and fixed SDK/tool paths; it preserves verification commands, scope conditions, permissions, archive validation, fallback behavior and failure exits.

The source verdict is favorable, with the inherited medium risk of the queue-to-main cache handoff. Workflow authorization for this PR is resolved. Current-head configured review, complete applicable CI and current-base native validation remain separate: older-head reviews and checks do not qualify this revision. The current-main infrastructure hold remains operative.

[Vilin97]

/review

Please run the configured refactor review for current published head 42edf1ef186a1cf09efc04622476545f679bbf44. The source continuation review is posted. This revision adds Exposition runner cleanup; the earlier 88f424351c65dbbcfbe3b615a169db96d736ed89 verdict and checks remain dated. Current-head CI and protected integration are separate.