[Vilin97]

Why

Out-of-disk crashes (System.IO.IOException: No space left on device) caused 63 of the last 126 failed jobs, mostly since Nov 4. Nearly all of them died in "Restore pool build": the whole-pool build cache is now ~7.5 GB compressed, and together with the 3 GB dependency cache it overflows a runner's default free space. Jobs with the "Free runner disk space" step (111 GB free afterwards) stopped crashing; the jobs without it kept dying.

Job	Disk crashes	Had cleanup?
Proof Profile: measure base/head	37	no
Proof Profile: profile added files	17	no
Daily documentation	4	added in #759
Exposition Verify	2	added in #740
Lean Action CI	3 (before Nov 3)	yes

The step was added one workflow at a time as each started failing, so the profiler never got it.

What

• Shared action .github/actions/free-disk-space, replacing the 7 inline copies in Lean Action CI, docs-build, docs-publish, and Exposition Verify.
• Proof Profile measure and absolute now free disk before restoring. These jobs check out the PR head, which may predate the shared action, so they keep an exact inline copy instead of uses: ./….
• Workflow Lint job "Free disk before pool-build restores" (python -m lean_pool.workflow_disk): fails when a job restores a LeanPoolBuild- cache (excluding lookup-only) before freeing disk, or when an inline copy drifts from the shared action. Dependency-only restores are exempt, since they never crashed.

Testing

• pytest tests/test_workflow_disk.py: 6 tests, including a check that the real workflows pass.
• Running the checker against current main reports exactly the two Proof Profile jobs.
• actionlint is clean on all workflows.
• Locally, test_notice.py::test_repository_notice_is_current and 3 test_stitched_logs_cannot_forge_later_file_headers cases also fail on unmodified main, so they're unrelated.

🤖 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; all previous findings are addressed and no new blocking issue was found.

Summary

The PR shares runner disk cleanup across build workflows, adds cleanup to Proof Profile, and adds a workflow check for cleanup before pool-build restores.

• Cache-using jobs clear unused runner tools before pool-build restores.
• Workflow Lint checks that pool-build restores have disk cleanup first.

_{Reviews (2) · Last reviewed commit: "Close three gaps in the pool-restore dis..." · Reviewed by Greptile}