ci: free up runner disk space before build - #13
Merged
Conversation
GitHub ubuntu-latest runners start with ~14 GB free disk. Our CI currently builds at least two Mathlib caches in a single job (the root project's via `lean-action@v1`, and a temp `two_plus_two` workspace's during `check_comparator_installation.py`), each ~7 GB of olean files. The subsequent `check_generated_builds.py` step would multiply this by the number of generated workspaces (each has its own `mathlib` dependency), making the problem worse. The net result: every main-branch CI run since 2026-04-12 has died with "No space left on device" before reaching the comparator installation or generated-builds steps. Add `jlumbroso/free-disk-space@v1.3.1` to reclaim ~30 GB of preinstalled tooling we don't use (Android SDK, .NET, Docker images, Haskell, large apt packages, swap). This buys enough headroom for multiple Mathlib caches plus the generated-workspaces build. The `tool-cache` option is left disabled because the runner uses it for Python, which we need for the CI scripts. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Brings the committed generated workspaces back in sync with the manifest and the current mathlib pin in lake-manifest.json: - Adds the 5 generated workspace directories that recent eval PRs (oppenheim, cayley, entrywise, normal product, catalan) committed source + manifest entries for but did not regenerate. - Updates the mathlib `rev` field in every existing workspace `lakefile.toml` from `v4.30.0-rc1` to `50d5513e83c` to match the bump in #9. - Updates `generated/index.json` accordingly. This unblocks `Run Eval Workflow Check` and `Verify Generated Output`, which both call `generate(check=True)` and were failing on these discrepancies once the disk-space crash was fixed. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
`run_eval.score_problems` computes `workspace_path.relative_to(gp.REPO_ROOT)`, which raises `ValueError` when the workspace path is outside `REPO_ROOT`. `evaluate_submission.py` already documents and works around this by putting its tempdir under `REPO_ROOT`. `check_eval_workflow.py` did not, so once CI got past the disk-space and missing-workspace issues it crashed here instead. Mirror the `evaluate_submission.py` pattern: pass `dir=gp.REPO_ROOT` to `tempfile.TemporaryDirectory`. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
When a problem is defined inside namespace blocks (e.g. `namespace FormalMathEval / namespace Combinatorics`), ChallengeDeps.lean wraps the extracted definitions in those namespaces. But Challenge.lean used unqualified names without opening those namespaces, causing "Unknown identifier" errors (e.g. `markoffGraph`). Fix `extract_context_opens` to track namespace/end blocks from the source file and emit a corresponding `open` statement. The open is only emitted when `ChallengeDeps.lean` exists (i.e. when the namespace is actually defined in the workspace); without ChallengeDeps, the namespace doesn't exist and `open` would error. Regenerated all workspaces. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1. Push trigger restricted to main only — branch pushes no longer fire a redundant CI run alongside the pull_request-triggered one. This halves the number of runs for every PR. 2. "Build Generated Workspaces" is now conditional on generated/ files actually changing. Problem-author PRs that only touch FormalMathEval/ and manifests/ skip the expensive workspace-build step entirely. 3. Shared Mathlib cache across generated workspaces — before building, a new step downloads Mathlib olean files once (via `lake update` + `lake exe cache get` in the first workspace), then hard-links the `.lake/packages/` tree into every other workspace. This turns 22 independent ~2 GB downloads into a single download + fast hard-link copies. Together these reduce typical PR CI from ~90 min / 2 runs down to ~15 min / 1 run for problem-author PRs, and from ~90 min × 2 to ~30 min × 1 for PRs that touch generated/ files. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Merge main into the CI fix branch and regenerate all workspaces to include the newly added problems (Schur-Weyl duality, exceptional Lie tensor squares, von Neumann DCT, Cerf gamma_4, and others). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
# Conflicts: # generated/index.json
The statement extractor used a non-greedy regex that matched the first
`:= by` in the declaration text. For theorems whose type contains
`haveI ... := by` clauses (e.g. `substInv_X_sub_X_sq_eq_catalan`),
this truncated the statement at the inner `:= by` instead of the
outer proof marker.
Use `rfind(":= by")` to locate the last occurrence, which is always
the outer proof start. Regenerated the affected workspace.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Summary
CI on
mainhas been failing on every run since 2026-04-12 withNo space left on deviceon the GitHub Actions runner. Root cause: within a single CI job, we build at least two Mathlib caches (~7 GB each):leanprover/lean-action@v1withuse-mathlib-cache: true— downloads and extracts olean files into./.lake/packages/mathlib/.scripts/check_comparator_installation.py— copiesgenerated/two_plus_twoto a tempdir, runslake exe cache getwhich downloads another ~7 GB of oleans.ubuntu-lateststarts with ~14 GB free, so these two alone saturate the disk. The subsequentcheck_generated_builds.pystep would multiply by the number of generated workspaces (each has its own Mathlib dependency), making things strictly worse. Every recent failure has died in exactly the same place: after "Run Evaluate Submission Tests" passes, before "Run Comparator Installation Checks" can finish.Adding
jlumbroso/free-disk-space@v1.3.1as the first step reclaims ~30 GB of preinstalled tooling we don't use (Android SDK, .NET, Docker images, Haskell, large apt packages, swap). That gives enough headroom for multiple Mathlib caches plus the generated-workspaces build.tool-cacheis left disabled because the runner uses it for Python, which we need for the CI scripts.Test plan
🤖 Generated with Claude Code