[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 blocking issues remain.

Summary

This PR moves seven repeated disk-cleanup scripts into one shared action and adds a check that cleanup comes before pool-cache restores.

• Most CI jobs now share one runner disk cleanup step.
• Workflow Lint checks disk cleanup before pool-build cache restores.

_{Reviews (5) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." · 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": []
}

[github-actions]

This PR has been open for 7 days and is now marked stale. Open PRs are closed automatically once they are 21 days old (and have been marked stale for at least 7 days).

[Vilin97]

Technical source approval at f163c2fcabaa45f4a7e7984ca5079375122a17df; no new material source finding.

I checked the complete nine-file change against current main, including the three workflows with newly integrated main edits. The action, checker and tests retain their reviewed source identities. Cleanup precedes the relevant restores, and the profiler keeps its exact inline script for checkouts that predate the action. The checker examines every restoring step; a covered conditional restore no longer hides a later uncovered restore.

The saved-source replay checks all 30 job records in the six changed workflows and rejects the second-uncovered-restore regression. This executed only selected pure checker functions on captured workflow data; it does not certify hosted workflow execution or transfer older-head CI.

Maintainability improves through one cleanup implementation and focused ordering/drift checks; risk is medium because the change introduces a validation gate. Current-head protected validation and the already identified direct authorization for this gate/workflow change remain separate requirements. I made no queue or auto-merge request.