chore: adaptations for nightly-2026-03-17#200

Closed

kim-em wants to merge 87 commits into

bump/v4.30.0from

bump/nightly-2026-03-17

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 13, 2026

Commits on Mar 16, 2026

Commits on Mar 17, 2026

Commits on Mar 18, 2026

chore: adaptations for nightly-2026-03-17
kim-em
committed