Zulip Chat Archive

Stream: CSLib

Topic: bump to v4.24.0


Chris Henson (Oct 14 2025 at 09:34):

With #30313 merged, there is a small bit of work in bumping to the new toolchain for the lambda calculus directory. I can handle this since I'm familiar. (And in general, I'm happy to do these PRs for incrementing the toolchain)

I'd also like to include the new mergeWithGrind linter as I mentioned in cslib#95, any objections?

Kim Morrison (Oct 14 2025 at 11:20):

My preference is actually that I do the toolchain bumps myself (as part of the bigger release process: it is much easier if one person can pull this off in one sitting, without having to coordinate).

This means that prior to the release, it's very helpful if CSLib main is already using a sufficiently recent version of Mathlib (because the release process will run lake update).

And similarly, if prior to the release of release candidates, any changes needed are already present on the nightly-testing branch. (But as I discovered today, the nightly-testing infrastructure wasn't actually working --- so we'll all learn this process together next month. :-)

Chris Henson (Oct 14 2025 at 11:35):

Okay, sorry for the hassle. It also doesn't help that my Mathib PR was just merged before the release. We had been updating Mathlib alongside toolchain updates, your preference is to be more frequent than this?

I have pushed the changes I had staged and the build is passing CI. There is an error in the linting action though, not sure what that is from. I tried updating to the commit Mathlib is using, but that didn't help.

Kim Morrison (Oct 14 2025 at 12:00):

Ideally, a lake update PR could happen (at least) shortly before release day. Usually release day is the 14th or 15th of each month. To date I've only been coordinating that date internally at the FRO, but I don't mind announcing it more publicly too!

Chris Henson (Oct 14 2025 at 12:08):

That sounds reasonable. I will plan to do a lake update a day or two before that then. And if we do have a situation like this month where code is moving from CSLib to Mathlib, I will be more cognizant of where that falls relative to the upcoming release so you aren't waiting on us.

(And thank you again for your patience this morning! I am glad I happen to be up early by a fluke...)


Last updated: Dec 20 2025 at 21:32 UTC