Zulip Chat Archive
Stream: Carleson
Topic: mathlib bump
Floris van Doorn (Jun 25 2024 at 21:35):
I don't really know how often I should bump Mathlib for a project like this (since it can be a little inconvenient), but I'm bumping Mathlib now (from v4.9.0-rc1 to v4.9.0-rc3). I'm planning to bump 1-2 times per month, but I could also do it more/less often. There were no fixes needed yet (that will probably be a temporary luxury).
Floris van Doorn (Jul 08 2024 at 13:20):
Just a heads-up: Pietro bumped mathlib again today.
Ruben Van de Velde (Apr 01 2025 at 14:42):
Bump to 4.18 is nearly done: https://github.com/fpvandoorn/carleson/pull/279 (help welcome)
Ruben Van de Velde (Apr 01 2025 at 16:00):
Should be clean now
Pietro Monticone (Apr 01 2025 at 16:45):
I just need to remove a lemma I have already upstreamed.
Pietro Monticone (Apr 01 2025 at 16:47):
Done.
Ruben Van de Velde (Apr 01 2025 at 17:23):
Thanks!
Floris van Doorn (Apr 01 2025 at 17:26):
Thanks for the bump!
Pietro Monticone (Apr 14 2025 at 17:17):
CI is failing because doc-gen hasn’t been updated to v4.19.0-rc3 yet.
I’ve already asked to update here so the failure it’s temporary and will fix itself soon.
Pietro Monticone (Apr 14 2025 at 17:19):
It has been bumped and I’ve re-run the job so we are good.
Jeremy Tan (Jun 02 2025 at 05:24):
(For fpvandoorn/carleson#359)
Ruben Van de Velde (Jul 01 2025 at 09:21):
Looking at v4.21
Ruben Van de Velde (Jul 01 2025 at 10:01):
CI is done on https://github.com/fpvandoorn/carleson/pull/424
Jeremy Tan (Jul 02 2025 at 02:34):
I bump mathlib to 4.22.0-rc2 in fpvandoorn/carleson#426. There are lots of unusedSimpArgs warnings fixed there
Jeremy Tan (Jul 02 2025 at 02:51):
CI has passed
Jeremy Tan (Jul 15 2025 at 02:17):
The bump to 4.22.0-rc3 in fpvandoorn/carleson#455 addresses the new commandStart linter
Jeremy Tan (Aug 07 2025 at 01:33):
For some reason I can't bump to the latest mathlib with just lake update in the top-level Carleson folder; I'm getting only
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
Current branch: HEAD
Using cache from origin: leanprover-community/mathlib4
No files to download
Decompressing 6982 file(s)
Unpacked in 401 ms
Completed successfully!
What is going on?
Pietro Monticone (Aug 07 2025 at 07:41):
You need to remove the pin from the lakefile.toml before bumping:
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
- rev = "v4.22.0-rc4"
Jeremy Tan (Aug 09 2025 at 05:47):
Jasper Mulder-Sohn (Aug 14 2025 at 11:05):
Michael Rothgang (Oct 24 2025 at 10:29):
I'm working on a bump to current mathlib now
Michael Rothgang (Oct 24 2025 at 13:00):
This is fpvandoorn/carleson#506 now: three proofs are broken; help fixing those is very welcome.
Michael Rothgang (Oct 24 2025 at 13:11):
I'm not working on this right now. If I pick this up again, I will write a message here.
Ruben Van de Velde (Oct 24 2025 at 21:31):
https://github.com/fpvandoorn/carleson/pull/508 for one of them (stopping now)
Michael Rothgang (Oct 30 2025 at 17:19):
fpvandoorn/carleson#511 bumps to current mathlib. This does not fix all warnings introduced e.g. by the SetLike (Finset) change; help fixing the remainder is welcome!
Michael Rothgang (Oct 30 2025 at 17:19):
I'll merge that PR soon, once CI has finished --- so PRs can be made directly against Carleson.
Jeremy Tan (Nov 01 2025 at 16:02):
fpvandoorn/carleson#513 fixes all remaining warnings (and removes a few of the lemmas I upstreamed)
Pietro Monticone (Nov 01 2025 at 18:03):
Jeremy Tan said:
fpvandoorn/carleson#513 fixes all remaining warnings (and removes a few of the lemmas I upstreamed)
Thanks. Reviewed and merged.
Jeremy Tan (Nov 01 2025 at 18:27):
I'd also like to have fpvandoorn/carleson#478 looked at again – I almost forgot about it after the project was finished
Pietro Monticone (Dec 16 2025 at 13:06):
Opened fpvandoorn/carleson#523 bumping to v4.27.0-rc1.
Last updated: Dec 20 2025 at 21:32 UTC