chore: adaptations for nightly-2026-03-24#202

Closed

kim-em wants to merge 233 commits into

bump/v4.30.0from

bump/nightly-2026-03-24

Commits on Feb 5, 2026

Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12325
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12325
leanprover-community-mathlib4-bot
committed

Commits on Feb 6, 2026

Update lean-toolchain for https://github.com/leanprover/lean4/pull/12325
leanprover-community-mathlib4-bot
committed

Commits on Feb 23, 2026

Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12662
leanprover-community-mathlib4-bot
committed

Commits on Feb 25, 2026

chore: adapt for inclusion of leading whitespace in input syntax
mhuisi
committed
chore: add Mathlib.Tactic exception
mhuisi
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12662
leanprover-community-mathlib4-bot
committed

Commits on Feb 26, 2026

chore: add module docstring linter special handling for eoi tokens
mhuisi
committed

Commits on Mar 3, 2026

Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12781
leanprover-community-mathlib4-bot
committed

Commits on Mar 4, 2026

Update lean-toolchain for https://github.com/leanprover/lean4/pull/12325
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12781
leanprover-community-mathlib4-bot
committed

Commits on Mar 5, 2026

rm stray file
kim-em
committed
Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
Merge branch 'nightly-testing' of https://github.com/leanprover-community/mathlib4-nightly-testing into nightly-testing
kim-em
committed
mk_all
kim-em
committed
Merge branch 'bump/nightly-2026-03-04' into nightly-testing
kim-em
committed
fixes
kim-em
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12325
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2026-03-05
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12805
leanprover-community-mathlib4-bot
committed
fix: address classDefReducibility warnings for lean4#12325

kim-em
and
claude
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12325
leanprover-community-mathlib4-bot
committed
fix: remove set_option/implicit_reducible from Setoid-typed defs

kim-em
and
claude
committed

Commits on Mar 6, 2026

Commits on Mar 7, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12805
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2026-03-07
mathlib-nightly-testing[bot]
committed
merge lean-pr-testing-12662
mathlib-nightly-testing[bot]
committed

Commits on Mar 8, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12841
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12841
leanprover-community-mathlib4-bot
committed

Commits on Mar 9, 2026

Commits on Mar 10, 2026

Commits on Mar 11, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12883
leanprover-community-mathlib4-bot
committed

Commits on Mar 12, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
chore: adapt to lean4#12698 (ExceptToEmoji → ExceptToTraceResult) and other nightly fixes
kim-em
committed
chore: remove manual emoji from withTraceNode callbacks (nightly adaptation)

kim-em
and
claude
committed
fix: close backtick after script name in scripts/README.md

kim-em
and
claude
committed
fix: replace toNat! with toNat? in version parsing to avoid panic

kim-em
and
claude
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12895
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12895
leanprover-community-mathlib4-bot
committed

Commits on Mar 13, 2026

Commits on Mar 15, 2026

Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12924
leanprover-community-mathlib4-bot
committed

Commits on Mar 16, 2026

Commits on Mar 17, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
fix merge
kim-em
committed
fix `inferInstanceAs` misuses
Kha
committed
chore: bump to nightly-2026-03-17
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12895
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12945
leanprover-community-mathlib4-bot
committed
fix
TwoFX
committed

Commits on Mar 18, 2026

chore: remove --rw /tmp landrun workaround for leantar

kim-em
and
claude
committed
Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
lake update batteries
kim-em
committed
adaptations for leanprover/lean4#12924
kim-em
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12897

leanprover-community-mathlib4-bot
authored and
kim-em
committed
fix

Kha
authored and
kim-em
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12895
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
fix more misuses
Kha
committed
chore: bump to nightly-2026-03-18
mathlib-nightly-testing[bot]
committed
merge lean-pr-testing-12945
mathlib-nightly-testing[bot]
committed
update aesop
Kha
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12895
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12973
leanprover-community-mathlib4-bot
committed

Commits on Mar 19, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12895
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12895
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12977
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2026-03-19
mathlib-nightly-testing[bot]
committed
fix: pass `allowOpaque := true` in `declUnfoldSimpAuxLemmas`

nomeata
and
claude
committed
merge lean-pr-testing-12924
mathlib-nightly-testing[bot]
committed
Fix
TwoFX
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12973
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
fix: pass `allowOpaque := true` in `@[simps]` to access theorem values

nomeata
and
claude
committed
fix: pass `allowOpaque := true` in `recall` to access theorem values

nomeata
and
claude
committed
merge lean-pr-testing-12895
Kha
committed
fix: pass `allowOpaque := true` in `#explode` and `to_dual` tests

nomeata
and
claude
committed
fix(script): make `add_set_option.py` idempotent
Kha
committed
49 new `set_option`s
Kha
committed
manual fix
Kha
committed
61 new `set_option`s
Kha
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
fixes for Mathlib.Data.ENat.Pow
kim-em
committed
fix OpenNhds
kim-em
committed
hacky: defeq abuse in MonoidAlgebra
kim-em
committed
add a noncomputable
kim-em
committed
some set_option backward
kim-em
committed

Commits on Mar 20, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
remove upstreamed
kim-em
committed
add some `noncomputable`
kim-em
committed
set_option backward
kim-em
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
working with everything disabled...
kim-em
committed
Merge branch 'lean-pr-testing-12897' of https://github.com/leanprover-community/mathlib4-nightly-testing into lean-pr-testing-12897
kim-em
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
build with backward.deriving.normalForm true
kim-em
committed
Merge branch 'lean-pr-testing-12897' of https://github.com/leanprover-community/mathlib4-nightly-testing into lean-pr-testing-12897
kim-em
committed
localizing backward.inferInstanceAs.normalize, and fixing some tests
kim-em
committed
turn off global inferInstanceAs.normalForm false; still two problems
kim-em
committed
one more set_option, probably indicating a bug
kim-em
committed
builds with no global set_options
kim-em
committed
cleanup lakefile
kim-em
committed
all localized
kim-em
committed
fix
kim-em
committed
Use «instance».normalForm.wrapFields.data where possible
kim-em
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13005
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13005
leanprover-community-mathlib4-bot
committed
rename options
Kha
committed
fix
Kha
committed
weaken backward option
Kha
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12987
leanprover-community-mathlib4-bot
committed
rm_set_option
kim-em
committed
megre
kim-em
committed
fix option name
kim-em
committed

Commits on Mar 21, 2026

Commits on Mar 22, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
a bit more minimization
kim-em
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
lake update batteries
kim-em
committed
Merge branch 'lean-pr-testing-12897' of https://github.com/leanprover-community/mathlib4-nightly-testing into lean-pr-testing-12897
kim-em
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12897
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12987
leanprover-community-mathlib4-bot
committed
Adapt
nomeata
committed
chore: bump to nightly-2026-03-22
mathlib-nightly-testing[bot]
committed
Merge branch 'nightly-testing' of github.com:leanprover-community/mathlib4-nightly-testing into nightly-testing
kim-em
committed
Merge branch 'lean-pr-testing-12897' of https://github.com/leanprover-community/mathlib4-nightly-testing into nightly-testing
kim-em
committed
merge lean-pr-testing-12897
kim-em
committed
lake update batteries
kim-em
committed
more meta
kim-em
committed
update option name
kim-em
committed
set_option
kim-em
committed
lake ipdate batteries
kim-em
committed
set_option
kim-em
committed
set_option
kim-em
committed
test output
kim-em
committed
don't need inferInstanceAs% anymore
kim-em
committed

Commits on Mar 23, 2026