[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; no actionable issues remain.

Summary

Shares runner disk cleanup across build and documentation jobs, keeps inline copies for Proof Profile, and adds a workflow check for cleanup before pool-build restores.

• Pool-cache jobs use a shared disk-cleanup action.
• Workflow Lint checks that pool-cache restores follow disk cleanup.

_{Reviews (4) · Last reviewed commit: "Check every pool-build restore in a job,..." · Reviewed by Greptile}

[Vilin97]

Changes requested at d629c1c0277e0dcb6afa583efd8699ec73c141fe: the new guard has one reproducible false negative.

job_errors breaks after the first pool-cache restore. A job with (1) cleanup conditioned on pushes, (2) a first restore with the same push condition, and (3) a later unconditional pool restore incorrectly returns no errors. On a pull request, the first pair is skipped and the later restore runs without cleanup. Removing the first restore from this fixture correctly produces an error, confirming that the early break hides the second restore.

Please check every restoring step and add this two-restore regression test. I independently checked the complete nine-file change; the shared action and the nine existing restore sites otherwise preserve the intended cleanup order. The ten published tests pass, but do not cover this case. Current authored CI is still pending.

This PR also adds a workflow validation gate and edits protected workflows, so it needs its own direct scoped authorization before protected integration under the contribution rules. The authorizations for the earlier workflow PRs do not cover this new gate.

[Vilin97]

{
"summary": "The current head fixes the earlier two-restore bypass: the checker now continues after a covered restore, and the added regression exercises a later uncovered restore. The shared cleanup action preserves the existing scripts and ordering; the two profiler jobs retain exact inline copies for older PR checkouts. This is a favorable technical source review; separate authorization for the protected gate change and current-head CI remain required.",
"assessment": {
"scope": "workflow cleanup extraction and checker regression fix",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "medium",
"assessment_one_sentence": "The reported bypass is resolved with a focused regression; no further material technical finding remains in the reviewed changes."
},
"verdict": "approve",
"findings": []
}