Commit 2026-01-26 23:03 5352afcc

View on Github →

chore: bump toolchain to v4.28.0-rc1 (#34436)

deprecation in lakefile
chore: bump to nightly-2025-12-10
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/11581
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/11587
chore: adaptations for nightly-2025-12-10
fix
fix for leanprover/lean4#11581
deprecation
remove unused argument
feat: register mathlib tactics with try? (#136) This PR adds register_try?_tactic calls for all finishing tactics currently registered with register_hint, which are not already covered by grind modules (i.e. I have not registered linarith or ring), using identical priority values: Common tactics (Common.lean):

tauto (priority 500)
aesop (priority 80)
fun_prop (priority 200) Domain-specific tactics:
norm_num (1000), noncomm_ring (1000)
field (850), bound (70)
finiteness (1000), compute_degree (1000), positivity (1000), field_simp (1000) 🤖 Prepared with Claude Code

chore: adaptations for nightly-2025-12-10 (#141)
fix deprecation in mk_all
chore: adaptations for nightly-2025-12-10
chore: bump to nightly-2025-12-11
Kick CI
lake update
fix deps
remove upstreamed
workaround
fix
chore: bump to nightly-2025-12-12
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/11620
more fix
fix the fix
lake update
adding a prime to NameMapExtension
adaptations for leanprover/lean4#11620
revert spurious change
warning
Merge master into nightly-testing
fixes
fix
deprecations
chore: bump to nightly-2025-12-13
lake update
lake update
fix merge
revert a lia back to omega
remove upstreamed
deprecation
fixes
fix archive
lint
lake update aesop
chore: adaptations for nightly-2025-12-13
remove aliases for upstreamed lemmas
deprecation
revert a lia back to omega
lake update
cutsat to lia
hm
note
adaptation notes
chore: bump to nightly-2025-12-14
remove @[grind =] from even_sign_iff
chore: adaptations for nightly-2025-12-13 (#142)
lake update
chore: adaptations for nightly-2025-12-14 (#143)
chore: adaptations for nightly-2025-12-14
chore: update lean-toolchain to leanprover/lean4:nightly-2025-12-14
chore: bump to nightly-2025-12-15
chore: adaptations for nightly-2025-12-15 (#144)
chore: bump to nightly-2025-12-16
Update batteries
Adapt to https://github.com/leanprover/lean4/pull/11608
Pull in aesop fixes (from my fork, sorry for that)
chore: adaptations for nightly-2025-12-16
fixes
chore: bump to nightly-2025-12-17
chore: adaptations for nightly-2025-12-17
chore: adaptations for nightly-2025-12-16 (#145)
chore: adaptations for nightly-2025-12-17 (#146)
chore: adaptations for nightly-2025-12-17
chore: bump to nightly-2025-12-18
lake update
chore: adaptations for nightly-2025-12-18
chore: bump to nightly-2025-12-19
remove upstreamed
remove upstreamed
fixes
chore: bump to nightly-2025-12-20
mk_all
chore: adaptations for nightly-2025-12-20
chore: adaptations for nightly-2025-12-20 (#148)
chore: adaptations for nightly-2025-12-20
chore: bump to nightly-2025-12-21
chore: adaptations for nightly-2025-12-21
chore: adaptations for nightly-2025-12-21 (#149)
chore: adaptations for nightly-2025-12-21
chore: bump to nightly-2025-12-22
chore: adaptations for nightly-2025-12-22
chore: bump to nightly-2025-12-23
chore: bump to nightly-2025-12-24
chore: adaptations for nightly-2025-12-24
chore: bump to nightly-2025-12-25
chore: adaptations for nightly-2025-12-25
chore: bump to nightly-2025-12-26
chore: adaptations for nightly-2025-12-26
chore: bump to nightly-2025-12-27
chore: bump to nightly-2025-12-28
chore: bump to nightly-2025-12-29
chore: bump to nightly-2025-12-30
chore: bump to nightly-2025-12-31
chore: bump to nightly-2026-01-01
chore: bump to nightly-2026-01-02
lake update
chore: bump to nightly-2026-01-03
chore: bump to nightly-2026-01-04
merge lean-pr-testing-10059
lake update
deprecations
Revert "merge lean-pr-testing-10387" This reverts commit e166d3308af8e8b87d9e6b7428c5767aeaa0440d, reversing changes made to cf6049c78aeba4176bfd4cf013afde27e2a9bc63.
fix
Revert incorrectly merged lean-pr-testing branches Reverts the following branches that were incorrectly merged due to a bug in discover-lean-pr-testing.yml where an empty prs.txt caused grep to match ALL lean-pr-testing branches:

lean-pr-testing-2714 (from Oct 2023!)
lean-pr-testing-11455
lean-pr-testing-11163
lean-pr-testing-10231
lean-pr-testing-10178
lean-pr-testing-10059 These PRs are not in nightly-2026-01-04, so their adaptations should not be merged. The bug fix is in: https://github.com/leanprover-community/mathlib4/pull/33546 🤖 Generated with Claude Code Co-Authored-By: Claude Opus 4.5 noreply@anthropic.com

deprecations
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/11893
fix
chore: bump to nightly-2026-01-05
remove upstreamed
lake update
fix
chore: adaptations for nightly-2026-01-05
chore: bump to nightly-2026-01-06
chore: adaptations for nightly-2026-01-06
chore: adaptations for nightly-2026-01-06
chore: bump to nightly-2026-01-07
chore: adaptations for nightly-2026-01-07
chore: adaptations for nightly-2026-01-09 (#159)
replace aesop proof
chore: adaptations for nightly-2026-01-07
chore: bump to nightly-2026-01-08
chore: adaptations for nightly-2026-01-08
chore: bump to nightly-2026-01-09

chore: adaptations for nightly-2026-01-23 (#160)
chore: adaptations for nightly-2026-01-24 (#161)
chore: adaptations for nightly-2026-01-25 (#162)
chore: bump toolchain to v4.28.0-rc1
fix: use main/master instead of nightly-testing for dependencies