diff --git a/.github/actions/free-disk-space/action.yml b/.github/actions/free-disk-space/action.yml new file mode 100644 index 0000000000..e12a01de12 --- /dev/null +++ b/.github/actions/free-disk-space/action.yml @@ -0,0 +1,16 @@ +name: Free runner disk space +description: >- + Delete preinstalled toolchains Lean Pool never uses (.NET, Android, GHC, + CodeQL, Swift), freeing about 25 GB. Without this, restoring the Lean + dependency cache plus the whole-pool build cache (about 8 GB compressed) + fails with "No space left on device". Run it before the first cache + restore; Workflow Lint enforces that. +runs: + using: composite + steps: + - name: Delete unused preinstalled toolchains + shell: bash + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ + /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift + df -h / diff --git a/.github/workflows/docs-build.yml b/.github/workflows/docs-build.yml index 7574c8d55d..b9b9ae3c72 100644 --- a/.github/workflows/docs-build.yml +++ b/.github/workflows/docs-build.yml @@ -36,13 +36,8 @@ jobs: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd with: persist-credentials: false - # The fresh main pool-build cache (about 8 GB compressed) plus the - # dependency cache overflow the runner's default free space. - name: Free runner disk space - run: | - sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ - /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift - df -h / + uses: ./.github/actions/free-disk-space - name: Restore Lean dependencies id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae diff --git a/.github/workflows/docs-publish.yml b/.github/workflows/docs-publish.yml index 88cfa07073..4198628b13 100644 --- a/.github/workflows/docs-publish.yml +++ b/.github/workflows/docs-publish.yml @@ -37,13 +37,8 @@ jobs: uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd with: persist-credentials: false - # The fresh main pool-build cache (about 8 GB compressed) plus the - # dependency cache overflow the runner's default free space. - name: Free runner disk space - run: | - sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ - /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift - df -h / + uses: ./.github/actions/free-disk-space - name: Restore Lean dependencies id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae diff --git a/.github/workflows/exposition-verify.yml b/.github/workflows/exposition-verify.yml index 432829f523..a3e6e004d7 100644 --- a/.github/workflows/exposition-verify.yml +++ b/.github/workflows/exposition-verify.yml @@ -101,13 +101,8 @@ jobs: id: build-identity run: echo "revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)" >> "$GITHUB_OUTPUT" - # The dependency and pool build caches together exceed the runner's - # default free space, so restoring them fails with ENOSPC. - name: Free runner disk space - run: | - sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ - /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift - df -h / + uses: ./.github/actions/free-disk-space # Match Lean Action CI's cache lookup exactly. This workflow only needs # compiled Lean artifacts; restoring doc-gen output here used to make a diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index bfd2038d1e..b19563f452 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -247,14 +247,8 @@ jobs: with: fetch-depth: 0 - # Restored caches plus the cache-save archive overflow the runner's - # default free space: every main build-cache save failed from - # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache. - name: Free runner disk space - run: | - sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ - /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift - df -h / + uses: ./.github/actions/free-disk-space # Keep the large toolchain/Mathlib cache independent of per-commit builds. - name: Restore Lean dependencies @@ -549,14 +543,8 @@ jobs: with: fetch-depth: 0 - # Restored caches plus the cache-save archive overflow the runner's - # default free space: every main build-cache save failed from - # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache. - name: Free runner disk space - run: | - sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ - /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift - df -h / + uses: ./.github/actions/free-disk-space - name: Restore Lean dependencies id: dependency-cache @@ -656,14 +644,8 @@ jobs: with: fetch-depth: 0 - # Restored caches plus the cache-save archive overflow the runner's - # default free space: every main build-cache save failed from - # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache. - name: Free runner disk space - run: | - sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ - /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift - df -h / + uses: ./.github/actions/free-disk-space - name: Restore Lean dependencies id: dependency-cache @@ -934,14 +916,8 @@ jobs: with: fetch-depth: 0 - # Restored caches plus the cache-save archive overflow the runner's - # default free space: every main build-cache save failed from - # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache. - name: Free runner disk space - run: | - sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ - /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift - df -h / + uses: ./.github/actions/free-disk-space - name: Restore Lean dependencies uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae diff --git a/.github/workflows/proof-profile.yml b/.github/workflows/proof-profile.yml index 393939d038..fb106ec720 100644 --- a/.github/workflows/proof-profile.yml +++ b/.github/workflows/proof-profile.yml @@ -275,6 +275,15 @@ jobs: fetch-depth: 0 persist-credentials: false + # Inline copy of .github/actions/free-disk-space: this job checks out + # the PR head, which may predate that action. Workflow Lint keeps the + # two identical. + - name: Free runner disk space + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ + /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift + df -h / + - name: Restore Lean dependencies id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -398,6 +407,15 @@ jobs: fetch-depth: 0 persist-credentials: false + # Inline copy of .github/actions/free-disk-space: this job checks out + # the PR head, which may predate that action. Workflow Lint keeps the + # two identical. + - name: Free runner disk space + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ + /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift + df -h / + - name: Restore Lean dependencies id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae diff --git a/.github/workflows/workflow_lint.yml b/.github/workflows/workflow_lint.yml index 7ed2c5aaf4..8b0d79ee36 100644 --- a/.github/workflows/workflow_lint.yml +++ b/.github/workflows/workflow_lint.yml @@ -90,3 +90,28 @@ jobs: - name: Ensure Actions are pinned uses: zgosalvez/github-actions-ensure-sha-pinned-actions@fc87bb5b5a97953d987372e74478de634726b3e5 + + disk-cleanup: + needs: scope + if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false') + runs-on: ubuntu-latest + name: Free disk before pool-build restores + steps: + - name: Require successful change classification + env: + SCOPE_RESULT: ${{ needs.scope.result }} + APPLICABLE: ${{ needs.scope.outputs.applicable }} + run: | + if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then + echo "::error::Change classification failed; required validation cannot be skipped." + exit 1 + fi + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + persist-credentials: false + + - name: Check disk cleanup precedes every pool-build restore + run: | + python3 -c 'import yaml' 2>/dev/null || sudo apt-get install -y python3-yaml + PYTHONPATH=python python3 -m lean_pool.workflow_disk diff --git a/python/lean_pool/workflow_disk.py b/python/lean_pool/workflow_disk.py new file mode 100644 index 0000000000..6a9ce96e35 --- /dev/null +++ b/python/lean_pool/workflow_disk.py @@ -0,0 +1,101 @@ +"""Require runner disk cleanup before any job restores the whole-pool build cache. + +The pool build cache (about 8 GB compressed) plus the Lean dependency cache do +not fit in a hosted runner's default free space, so a job that restores it +without first deleting unused preinstalled toolchains dies with "No space left +on device". This check fails Workflow Lint when a job skips that cleanup. +""" + +from __future__ import annotations + +import argparse +from pathlib import Path +from typing import Any + +import yaml + +ACTION_PATH = Path(".github/actions/free-disk-space/action.yml") +ACTION_REFERENCE = "./.github/actions/free-disk-space" +POOL_BUILD_CACHE_PREFIX = "LeanPoolBuild-" +CLEANUP_MARKER = "sudo rm -rf /usr/share/dotnet" +RESTORING_ACTIONS = ("actions/cache@", "actions/cache/restore@") + + +def cleanup_script(root: Path) -> str: + """Return the shell script the shared free-disk-space action runs.""" + action = yaml.safe_load((root / ACTION_PATH).read_text()) + return action["runs"]["steps"][0]["run"].strip() + + +def restores_pool_build(step: dict[str, Any]) -> bool: + """Whether a step downloads the whole-pool build cache onto the runner.""" + if not str(step.get("uses", "")).startswith(RESTORING_ACTIONS): + return False + settings = step.get("with") or {} + if settings.get("lookup-only") in (True, "true"): + return False + keys = f"{settings.get('key', '')}\n{settings.get('restore-keys', '')}" + return POOL_BUILD_CACHE_PREFIX in keys + + +def frees_disk(step: dict[str, Any], script: str) -> bool: + """Whether a step runs the shared cleanup, as the action or an exact copy.""" + if step.get("uses") == ACTION_REFERENCE: + return True + return str(step.get("run", "")).strip() == script + + +def job_errors(location: str, steps: list[dict[str, Any]], script: str) -> list[str]: + """Report a missing, late, or drifted cleanup step in one job.""" + errors = [] + for step in steps: + run = str(step.get("run", "")) + if CLEANUP_MARKER in run and run.strip() != script: + errors.append( + f"{location}: inline disk cleanup differs from {ACTION_PATH}; " + f"use `uses: {ACTION_REFERENCE}` or copy its script exactly" + ) + cleanup_conditions = [] + for step in steps: + if frees_disk(step, script): + cleanup_conditions.append(step.get("if")) + elif restores_pool_build(step): + # A conditional cleanup only covers a restore with the same condition. + if not {None, step.get("if")} & set(cleanup_conditions): + errors.append( + f"{location}: step {step.get('name', step['uses'])!r} " + f"restores the pool build cache without an earlier cleanup " + f"that always runs with it; add `uses: {ACTION_REFERENCE}` " + f"after checkout" + ) + break + return errors + + +def workflow_errors(root: Path) -> list[str]: + """Check every job in every workflow under ``root``.""" + script = cleanup_script(root) + errors = [] + for path in sorted((root / ".github/workflows").glob("*.y*ml")): + workflow = yaml.safe_load(path.read_text()) or {} + for name, job in (workflow.get("jobs") or {}).items(): + location = f"{path.relative_to(root)} job {name}" + errors.extend(job_errors(location, job.get("steps") or [], script)) + return errors + + +def main() -> None: + """Fail when a workflow job restores the pool build without freeing disk.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=Path.cwd()) + arguments = parser.parse_args() + errors = workflow_errors(arguments.root) + if errors: + for error in errors: + print(f"::error::{error}") + raise SystemExit(1) + print("Every job frees runner disk before restoring the pool build cache") + + +if __name__ == "__main__": + main() diff --git a/python/tests/test_workflow_disk.py b/python/tests/test_workflow_disk.py new file mode 100644 index 0000000000..ae98b7b8e9 --- /dev/null +++ b/python/tests/test_workflow_disk.py @@ -0,0 +1,111 @@ +"""Coverage for the free-disk-before-pool-restore workflow check.""" + +from pathlib import Path + +import yaml + +from lean_pool.workflow_disk import ACTION_PATH, workflow_errors + +REPOSITORY = Path(__file__).resolve().parents[2] +SCRIPT = "sudo rm -rf /usr/share/dotnet /usr/local/lib/android\ndf -h /\n" +CHECKOUT = {"uses": "actions/checkout@sha"} +FREE = {"name": "Free runner disk space", "uses": "./.github/actions/free-disk-space"} +RESTORE = { + "name": "Restore pool build", + "uses": "actions/cache/restore@sha", + "with": {"path": ".lake/build", "key": "LeanPoolBuild-v1-Linux-abc"}, +} + + +def write_repository(root: Path, steps: list[dict]) -> Path: + """Create a repository with the shared action and one single-job workflow.""" + action = root / ACTION_PATH + action.parent.mkdir(parents=True) + action.write_text( + yaml.safe_dump( + {"runs": {"using": "composite", "steps": [{"run": SCRIPT}]}}, + ) + ) + workflows = root / ".github/workflows" + workflows.mkdir(parents=True) + (workflows / "build.yml").write_text( + yaml.safe_dump({"jobs": {"build": {"steps": steps}}}) + ) + return root + + +def test_repository_workflows_free_disk_before_pool_restore(): + """Every real workflow passes, so the gate starts green.""" + assert workflow_errors(REPOSITORY) == [] + + +def test_restore_without_cleanup_fails(tmp_path): + """A job that restores the pool build without cleanup is reported.""" + errors = workflow_errors(write_repository(tmp_path, [CHECKOUT, RESTORE])) + assert len(errors) == 1 + assert "without an earlier cleanup" in errors[0] + + +def test_cleanup_after_restore_fails(tmp_path): + """Cleanup must come before the restore, not after it.""" + errors = workflow_errors(write_repository(tmp_path, [CHECKOUT, RESTORE, FREE])) + assert len(errors) == 1 + + +def test_shared_action_or_exact_inline_copy_passes(tmp_path): + """Both the shared action and an identical inline script are accepted.""" + inline = {"name": "Free runner disk space", "run": SCRIPT} + assert workflow_errors(write_repository(tmp_path / "a", [FREE, RESTORE])) == [] + assert workflow_errors(write_repository(tmp_path / "b", [inline, RESTORE])) == [] + + +def test_drifted_inline_copy_fails(tmp_path): + """An inline cleanup that no longer matches the shared action is reported.""" + drifted = {"run": "sudo rm -rf /usr/share/dotnet\ndf -h /\n"} + errors = workflow_errors(write_repository(tmp_path, [drifted, RESTORE])) + assert any("differs from" in error for error in errors) + + +def test_lookup_only_and_other_caches_are_exempt(tmp_path): + """Lookups download nothing, and the dependency cache alone fits on disk.""" + lookup = {**RESTORE, "with": {**RESTORE["with"], "lookup-only": True}} + dependencies = { + "uses": "actions/cache/restore@sha", + "with": {"path": ".lake/packages", "key": "LeanDependencies-v1-Linux-abc"}, + } + root = write_repository(tmp_path, [CHECKOUT, lookup, dependencies]) + assert workflow_errors(root) == [] + + +def test_conditional_cleanup_does_not_cover_unconditional_restore(tmp_path): + """Cleanup skipped on some events leaves those restores unprotected.""" + conditional = {**FREE, "if": "github.event_name == 'push'"} + errors = workflow_errors(write_repository(tmp_path, [conditional, RESTORE])) + assert len(errors) == 1 + + +def test_cleanup_with_the_restores_condition_passes(tmp_path): + """A cleanup gated exactly like its restore always runs alongside it.""" + condition = "github.event_name == 'push'" + steps = [{**FREE, "if": condition}, {**RESTORE, "if": condition}] + assert workflow_errors(write_repository(tmp_path, steps)) == [] + + +def test_pool_build_fallback_key_counts_as_a_restore(tmp_path): + """A pool build restored through `restore-keys` still needs cleanup.""" + fallback = { + **RESTORE, + "with": { + "path": ".lake/build", + "key": "Other-v1-abc", + "restore-keys": "LeanPoolBuild-v1-Linux-\n", + }, + } + errors = workflow_errors(write_repository(tmp_path, [CHECKOUT, fallback])) + assert len(errors) == 1 + + +def test_save_only_steps_are_exempt(tmp_path): + """Saving uploads the build; it downloads nothing onto the runner.""" + save = {**RESTORE, "uses": "actions/cache/save@sha"} + assert workflow_errors(write_repository(tmp_path, [CHECKOUT, save])) == []