chore: bump mathlib to 50d5513e83c - #9
Merged
Merged
Conversation
Picks up recent additions including: - Schur product theorem (PosSemidef.hadamard) from PR #37297 - Fuglede-Putnam-Rosenblum theorem from PR #37569 - Power series compositional inverse (substInv) from PR #26645 - Cayley graph definition from PR #35084 - Formal group laws from PR #35912 Same Lean toolchain (v4.30.0-rc1), no toolchain change. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
kim-em
added a commit
that referenced
this pull request
Apr 16, 2026
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>
kim-em
added a commit
that referenced
this pull request
Apr 17, 2026
* ci: free up runner disk space before build 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> * chore(generated): regenerate workspaces 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> * fix(scripts): place workflow-check tempdir under REPO_ROOT `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> * fix(generator): emit open for enclosing namespaces in Challenge.lean 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> * ci: reduce CI cost with three optimizations 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> * chore(generated): regenerate after merging main 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> * fix(generator): use last := by when extracting theorem statements 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> --------- 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
v4.30.0-rc1to50d5513e83c(same Lean toolchain)🤖 Prepared with Claude Code