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.

Last updated: May 02 2025 at 03:31 UTC