chore: adaptations for nightly-2025-05-01#24524

Merged

kim-em merged 6230 commits intobump/v4.20.0from

bump/nightly-2025-05-01

May 2, 2025

This pull request is big! We're only showing the most recent 250 commits

Commits on Apr 15, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Trigger CI for https://github.com/leanprover/lean4/pull/7971
leanprover-community-mathlib4-bot
committed
WIP
TwoFX
committed
WIP
TwoFX
committed
WIP
TwoFX
committed
Trigger CI for https://github.com/leanprover/lean4/pull/7971
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/7975
leanprover-community-mathlib4-bot
committed
Fix
TwoFX
committed
Trigger CI for https://github.com/leanprover/lean4/pull/7971
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on Apr 16, 2025

remove adaptation notes
kim-em
committed
Fix
TwoFX
committed
Fix
TwoFX
committed
Trigger CI for https://github.com/leanprover/lean4/pull/7855
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-16
leanprover-community-mathlib4-bot
committed
merge lean-pr-testing-7933
github-actions
committed
merge lean-pr-testing-7975
github-actions
committed
revert some stuff
Rob23oba
committed
Merge branch 'lean-pr-testing-7855' of https://github.com/leanprover-community/mathlib4 into lean-pr-testing-7855
Rob23oba
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/7983
leanprover-community-mathlib4-bot
committed
WIP
TwoFX
committed
Part one
TwoFX
committed
Part two
TwoFX
committed
lake update and fix
TwoFX
committed
Fix
TwoFX
committed
Trigger CI for https://github.com/leanprover/lean4/pull/7983
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Shake
TwoFX
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on Apr 17, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-17
leanprover-community-mathlib4-bot
committed
merge lean-pr-testing-7855
github-actions
committed
merge lean-pr-testing-7983
github-actions
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
merge lean-pr-testing-7971
kim-em
committed
lake update
kim-em
committed
.
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on Apr 18, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-18
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/8021
leanprover-community-mathlib4-bot
committed
fix
Kha
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix: !bench after Lake path changes (#24143)
Kha
authored
fix
Kha
committed
fix
Kha
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on Apr 19, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-19
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: adaptations for nightly-2025-04-16
kmill
committed
Merge branch 'bump/nightly-2025-04-16' into nightly-testing
kmill
committed
temporarirly disable sythorder checking for Grind.IsCharP instance
kmill
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
shake
kmill
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: adaptations for nightly-2025-04-19
kmill
committed
Merge branch 'bump/nightly-2025-04-19' into nightly-testing
kmill
committed

Commits on Apr 20, 2025

chore: bump to nightly-2025-04-20
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: adaptations for nightly-2025-04-20
kim-em
committed
Merge branch 'bump/nightly-2025-04-20' into nightly-testing
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix
Kha
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Trigger CI for https://github.com/leanprover/lean4/pull/8021
leanprover-community-mathlib4-bot
committed

Commits on Apr 21, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-21
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
make fix more robust
Kha
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix test
kim-em
committed

Commits on Apr 22, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: adaptations for nightly-2025-04-21
kim-em
committed
Merge branch 'bump/nightly-2025-04-21' into nightly-testing
kim-em
committed
chore: bump to nightly-2025-04-22
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
merge lean-pr-testing-6432
kim-em
committed
.
kim-em
committed
merge lean-pr-testing-8021
kim-em
committed
sorries
kim-em
committed
sorries
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on Apr 23, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-23
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on Apr 24, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-24
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
not there yet
kim-em
committed
comment out
kim-em
committed
Merge branch 'nightly-testing' of github.com:leanprover-community/mathlib4 into nightly-testing
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
comment out
kim-em
committed
Merge branch 'nightly-testing' of github.com:leanprover-community/mathlib4 into nightly-testing
kim-em
committed

Commits on Apr 25, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-25
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge branch 'nightly-testing' of github.com:leanprover-community/mathlib4 into nightly-testing
kim-em
committed
bump batteries
kim-em
committed
more
kim-em
committed
hacky fix?
kim-em
committed
add comment
kim-em
committed
fix lint-style
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Fix shake: Parser.parseHeader returns TSyntax instead of Syntax after the new module system
TwoFX
committed
Clean up
TwoFX
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/8000
leanprover-community-mathlib4-bot
committed
Lake update
TwoFX
committed
Fix
TwoFX
committed
Fix
TwoFX
committed
Fix
TwoFX
committed
Fix
TwoFX
committed
fix to Mathlib/Algebra/Homology/Embedding/Connect.lean
joelriou
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Fix
TwoFX
committed

Commits on Apr 26, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-26
leanprover-community-mathlib4-bot
committed
merge lean-pr-testing-8000
github-actions
committed
fix MinImports
Kha
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/8114
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
lake update
kim-em
committed
Trigger CI for https://github.com/leanprover/lean4/pull/8114
leanprover-community-mathlib4-bot
committed
fix
kim-em
committed
fixes
kim-em
committed
fix
kim-em
committed
fix deprecations
Kha
committed
remove accidental files
Kha
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge branch 'lean-pr-testing-8114' into nightly-testing
Kha
committed
chore: bump to nightly-2025-04-26
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on Apr 27, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-27
leanprover-community-mathlib4-bot
committed
chore: adaptations for nightly-2025-04-26
kim-em
committed
Merge branch 'bump/nightly-2025-04-26' into nightly-testing
kim-em
committed
fixes
kim-em
committed
cleanup adaptation note
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
shake --fix
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
merge
kim-em
committed
cleanup
kim-em
committed
.
kim-em
committed
cleanup
kim-em
committed
cleanup
kim-em
committed
cleanup
kim-em
committed
comments
kim-em
committed
cleanuo
kim-em
committed
move batteries back to nightly-testing
kim-em
committed
merge
kim-em
committed
fix
Ruben-VandeVelde
committed
chore: adaptations for nightly-2025-04-27
kim-em
committed

Commits on Apr 28, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix build hopefully?
jcommelin
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix build hopefully?
jcommelin
committed
chore: bump to nightly-2025-04-28
leanprover-community-mathlib4-bot
committed
chore: adaptations for nightly-2025-04-28
jcommelin
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/8144
leanprover-community-mathlib4-bot
committed
lake update
TwoFX
committed
Fix
TwoFX
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix grind instances
kim-em
committed
Merge branch 'nightly-testing' of github.com:leanprover-community/mathlib4 into nightly-testing
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
shake
Ruben-VandeVelde
committed
Merge remote-tracking branch 'origin/master' into nightly-testing
Ruben-VandeVelde
committed
Cleanup
Ruben-VandeVelde
committed
shake
Ruben-VandeVelde
committed

Commits on Apr 29, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-29
leanprover-community-mathlib4-bot
committed
merge lean-pr-testing-8144
github-actions
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix
jcommelin
committed
deprecation
kim-em
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/8161
leanprover-community-mathlib4-bot
committed
shake
jcommelin
committed
fix GrindInstances
kim-em
committed
basic test for grind +ring
kim-em
committed
fixes for leanprover/lean4#8161
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fixes
kim-em
committed
Merge commit '5afdea540abf6226b130896e2c1ae3e06de1c3bb' into bump/nightly-2025-04-29
jcommelin
committed
chore: adaptations for nightly-2025-04-29
jcommelin
committed
Merge branch 'bump/nightly-2025-04-29' into nightly-testing
jcommelin
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on Apr 30, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2025-04-30
leanprover-community-mathlib4-bot
committed
merge lean-pr-testing-8161
kim-em
committed
lake update
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix
Ruben-VandeVelde
committed
fix merge
kim-em
committed
fix merge
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Drop a few unnecessary changes
Ruben-VandeVelde
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
chore: adaptations for nightly-2025-04-30
kim-em
committed
Merge remote-tracking branch 'origin/bump/nightly-2025-04-30' into nightly-testing
kim-em
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed

Commits on May 1, 2025

Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix test
kim-em
committed
chore: bump to nightly-2025-05-01
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
leanprover-community-mathlib4-bot
committed
fix
kim-em
committed
chore: adaptations for nightly-2025-05-01
kim-em
committed