Repository navigation
Free runner disk before every pool-build restore and lint for it #764
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
Vilin97
wants to merge
4
commits into
main
Choose a base branch
from
vasil/free-disk-everywhere
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
+273
−50
Open
Changes from all commits
Commits
Show all changes
4 commits
Select commit
Hold shift + click to select a range
3da4bf6
Free runner disk before every pool-build restore and lint for it
Vilin97 d629c1c
Close three gaps in the pool-restore disk check
Vilin97 647352c
Merge remote-tracking branch 'origin/main' into vasil/free-disk-every…
Vilin97 469f54d
Check every pool-build restore in a job, not only the first
Vilin97 File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 / |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,100 @@ | ||
| """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" | ||
| ) | ||
| 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() | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,119 @@ | ||
| """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])) == [] | ||
|
|
||
|
|
||
| def test_every_restore_is_checked_not_only_the_first(tmp_path): | ||
| """A covered conditional restore does not excuse a later unconditional one.""" | ||
| condition = "github.event_name == 'push'" | ||
| steps = [{**FREE, "if": condition}, {**RESTORE, "if": condition}, RESTORE] | ||
| errors = workflow_errors(write_repository(tmp_path, steps)) | ||
| assert len(errors) == 1 |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.