chore: adaptations for nightly-2026-03-17#200
Open
kim-em wants to merge 87 commits intobump/v4.30.0from
Open
Conversation
Add `@[implicit_reducible]` to class-typed `def`s where safe, and disable the warning with `set_option warn.classDefReducibility false in` where adding the attribute causes downstream breakage. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The new toolchain version of lean4#12325 exempts `Setoid` from the classDefReducibility warning, so these suppressions are no longer needed. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… other nightly fixes
…tation) withTraceNode now auto-prepends emoji based on TraceResult, so manual emoji in callbacks cause doubled output. Remove them from Notation.lean, Normalize.lean, PureCoherence.lean, DepRewrite.lean, FieldSimp/Discharger. Update test #guard_msgs accordingly: ❌️ → 💥️ for failed strategies, ✅️ added to cleanupCasts trace headers, [✅️] → ✅️ for fun_prop. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The lint-style checker looks for `scriptname` (backtick-enclosed filename) in the README. The grind_unused_lemmas.sh entry had the arguments inside the backticks, so the linter couldn't find `grind_unused_lemmas.sh`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The nightly-2026-03-10 toolchain bundles leantar, whose `--version` output includes a trailing newline. This caused `parseVersion` to call `toNat!` on "18\n", triggering a panic. Using `toNat?` with proper error handling avoids the crash. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Since nightly-2026-03-09 (lean4#12822), Lean ships `leantar` in its sysroot at `$(lean --print-prefix)/bin/leantar`. Use that version if available, so leantar is always in sync with the toolchain. Fall back to the existing download logic for older toolchains. This fixes the "bad .trace file" leantar panic seen with nightly-2026-03-14 when using the previously-cached leantar-0.1.16. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…leantar Since nightly-2026-03-09 leantar is bundled with the Lean toolchain. The fallback download logic is no longer needed and would fail anyway with newer versions. Hard-fail at startup if the sysroot binary is absent.
Remove Version/parseVersion (only used for leantar version checks) and validateLeanTar/its call site (redundant since leantarSysrootBin already throws at module init if leantar is absent).
leantar v0.1.18 (bundled with Lean) uses tempfile::NamedTempFile::new() which unconditionally writes to /tmp, but landrun blocks /tmp access. This is a temporary workaround until leantar is fixed. See: digama0/leangz@6d1691e0a4 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Author
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 18, 2026
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
|
Build failed: |
kim-em
force-pushed
the
bump/v4.30.0
branch
2 times, most recently
from
35638f9 to
5179ef5
Compare
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
4 participants
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.
No description provided.