lean#5144 and leangz

Stream: lean4

[Kim Morrison]

@Mario Carneiro, I'm happy to let you decide when exactly we merge lean#5144. I've just rebased it and hopefully it is ready to go, but as you say, we shouldn't merge until leangz is ready.

I'm currently hoping to cut v4.14.0-rc1 from nightly-2024-11-01, 02, or 03, depending on how my weekend goes. If we can get it into one of those that would be great.

[Mario Carneiro]

So to clarify, the versions that will exist prior to the fix are v4.13.0-rcN and v4.13.0?

[Mario Carneiro]

Doing this around the time of a major version release is actually a bit awkward because I want to release after I know the git SHA of the last regular or RC version that will be on olean-v1

[Mario Carneiro]

if you can release v4.13.0 with a small gap before v4.14.0-rc1 that would work

[Kim Morrison]

Should be no problem. I'm thinking to do 4.13.0 on my Friday, v4.14.0-rc1 on my Monday.

[Kim Morrison]

If that's okay I'll send in lean#5144 to master shortly.

[Kim Morrison]

@Mario Carneiro, v4.13.0 is cut now.

[Mario Carneiro]

@Sebastian Ullrich I guess the issue here is now important to look at soon. I think it is okay if we decide not to fix it now, but once olean-v2 is released we won't be able to consider backward incompatible fixes.

[Kim Morrison]

(Just noting I'll be offline for 48 hours, but in any case I'm hopefully not needed on this one. :-)

[Sebastian Ullrich]

I'd advocate for a -pre suffix, i.e. no header changes necessary

[Kim Morrison]

Is this something you can do, @Sebastian Ullrich? If I understand right this involves touching the CMakeLists file, which I'm still afraid of. :-)

[Sebastian Ullrich]

Yeah I can do it next week

[Mario Carneiro]

ok, in that case I will go ahead with the release

[Mario Carneiro]

leangz v0.1.14 is ready in #18514

[Mario Carneiro]

as usual, it can be merged independently of the lean change

[Kim Morrison]

Sebastian Ullrich said:

Yeah I can do it next week

Sorry, @Sebastian Ullrich or @Mario Carneiro, is this step a blocker for releasing v4.14.0-rc1? (Okay if so, I'm just not certain.)

[Mario Carneiro]

No, it should be okay to proceed. The consequence of the bug is that leangz may get confused about migrations involving nightly or custom toolchains but neither migrations nor custom toolchains are commonly used so it is a low priority bug to fix. (It was high priority to determine whether the bug should be fixed in a backward incompatible way, but since @Sebastian Ullrich decided on a backward compatible fix, it's fine to happen whenever.)

[Sebastian Ullrich]

lean#5943

[Siddhartha Gadgil]

I have not seen an announcement, so was wondering whether to take v4.13.0 as released for Mathlib+toolchain+... or to wait a bit.

[Kim Morrison]

No announcement yet, but it is indeed out, and Mathlib has a v4.13.0 tag using it.