[Vilin97]

The advisory proof profiler fails on every PR: the Measure head/base NN jobs die in Restore pool build with System.IO.IOException: No space left on device (e.g. run 42064834858 on #756/#757), and the comment then reads "No proof profile output.".

This adds the same Free runner disk space step that lean_action_ci.yml already uses (removes dotnet, Android SDK, GHC, CodeQL, Swift; prints df -h /) to the two jobs that restore the pool build — measure and absolute — right after checkout, before the dependency and pool-build restores. Nothing else changes; the plan and report jobs don't restore caches.

Infra-only; no LeanPool/** changes. The profiler is advisory, so this doesn't touch any merge gate.

Checks: actionlint clean; pytest tests/test_ci_cache_contract.py tests/test_proof_profile_workflow.py → 85 passed.

Verification: dispatched the profiler from this branch (workflow_dispatch, so it uses this PR's workflow file) against the two PRs that were failing:

• Split over-long proofs in AndersonConjecture #756 — run 42085751897: plan, measure base 00, measure head 00 and report all succeeded. 111 GB free after cleanup; Restore pool build restored the full LeanPoolBuild-v1-… cache. The comment now shows the base→head table (12 files, heartbeats 1,846,008 → 2,037,621).
• Split over-long proofs in PLAcceleratedNesterovLean #757 — run 42085757023: same result; the comment shows 4 modified files compared (−19.6% heartbeats) plus the new-file absolute profile.

An earlier dispatch on #742 also exercised the absolute job (cleanup step plus restores) and passed.

🤖 Generated with Claude Code

[greptile-apps]

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

[Low impact] This PR appears safe to merge.

Summary

Adds disk cleanup before cache downloads in measure and absolute.

• Proof-profile jobs clear runner disk before restoring Lean caches.

No actionable issues found. Runner disk recovery was not tested during this review.

_{Reviews (1) · Last reviewed commit: "ci(proof-profile): free runner disk befo..." · Reviewed by Greptile}

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

[Vilin97]

{
"assessment": {
"assessment_one_sentence": "The two inserted cleanup steps reuse the exact main-CI command and leave cache identities, measurement inputs, token permissions and advisory reporting unchanged.",
"brittleness": "more_robust",
"introduces_tech_debt": false,
"maintainability": "improved",
"risk": "low",
"scope": "Complete published old/head proof-profile.yml at7c5b98bb7ba663928290250350212e1f23f556ce; infrastructure only."
},
"findings": [],
"summary": "Free fixed hosted-runner tool bundles before restoring dependency and pool-build caches in both advisory profiling jobs. This is a technical source verdict; the repository rule requires separate direct authorization for this PR's workflow changes before protected integration, followed by its normal applicable checks.",
"verdict": "approve"
}

[Vilin97]

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

Reviewed head: 7c5b98bb7ba663928290250350212e1f23f556ce

Verdict: ✅ approve

Adds the existing CI disk cleanup before dependency and pool-build restores in both profiling jobs. The commands match lean_action_ci.yml; Lean sources, cache contracts, and job conditions remain unchanged. All 85 targeted tests and cleanup shell syntax checks passed. Hosted-runner disk recovery remains unverified; actionlint was unavailable locally.

Aspect	Value
Scope	CI disk cleanup
Introduces tech debt	✅ no
Maintainability	➖ unchanged
Brittleness	➖ unchanged
Risk	✅ low

The cleanup follows the established CI setup and introduces no actionable maintenance debt.

---

Tokens: 489,453 in / 4,896 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $2.0313 (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.