Stream: general

Topic: v4.21.0-rc3

Wrenna Robson (Jun 05 2025 at 08:19):

The link appears to be dead for me - am I just too keen?

Anne Baanen (Jun 05 2025 at 08:20):

Wrenna Robson said:

The link appears to be dead for me - am I just too keen?

Sorry, a copy/paste error. Thanks for spotting, should be fixed now!

Notification Bot (Jun 05 2025 at 08:21):

2 messages were moved here from #announce > v4.21.0-rc3 by Anne Baanen.

Wrenna Robson (Jun 05 2025 at 08:21):

Oh, apologies for replying in the wrong place! Thanks for the fix.

Anne Baanen (Jun 05 2025 at 08:23):

No worries at all! We like to keep the announce threads short, but it was better to get this fixed quickly :)

Wrenna Robson (Jun 05 2025 at 08:23):

lean4#8291 is nice

Wrenna Robson (Jun 05 2025 at 08:24):

... though I would argue that zero_lt_one and castSucc_one could have been changed.

Wrenna Robson (Jun 05 2025 at 08:33):

I adore all the improvements in Array in the last year or so.

Jovan Gerbscheid (Jun 05 2025 at 10:06):

I think the release notes are missing lean#7428. This is what gave the major simp performance improvement.

Kim Morrison (Jun 05 2025 at 10:59):

@Anne Baanen, could you track down why this is missing in the release notes, and make sure it gets in? We definitely want to acknowledge that one!

Sebastian Ullrich (Jun 05 2025 at 11:15):

Likely because it doesn't have a changelog- label. We don't force one for perf: commit... yet?

Kim Morrison (Jun 05 2025 at 11:20):

Yes, let's. It's a shame to miss these from the release notes.

Anne Baanen (Jun 05 2025 at 12:28):

Jovan Gerbscheid said:

I think the release notes are missing lean#7428. This is what gave the major simp performance improvement.

We should definitely include that! I have opened a PR to mention this in the release notes. If it looks good to you, feel free to rebase-merge: https://github.com/leanprover/reference-manual/pull/462

Yaël Dillies (Jun 30 2025 at 08:33):

v4.21.0

Yaël Dillies (Jun 30 2025 at 08:35):

I encountered a weird issue I had never seen before. Here is how to reproduce:

Clone https://github.com/YaelDillies/Toric
Checkout 6537a03
Pin the version of mathlib to v4.21.0 in the TOML
Run lake update
Run lake build

Yaël Dillies (Jun 30 2025 at 08:35):

Instead of building Toric as expected, it rebuilds batteries, mathlib, etc...

Yaël Dillies (Jun 30 2025 at 08:36):

If you further do:

Cancel the build
rm -rf .lake
lake exe cache get
lake build

Yaël Dillies (Jun 30 2025 at 08:36):

then things work as expected. What's going on?

Ruben Van de Velde (Jun 30 2025 at 08:39):

Same in PNT+ and sphere-eversion (though I used get! in 8 without trying plain get first)

Sebastian Ullrich (Jun 30 2025 at 08:48):

I'll try reproducing but in the meantime - what's the previous version you know that worked, 4.20.0?

Ruben Van de Velde (Jun 30 2025 at 08:52):

I bumped straight from 4.20.0, yeah

Sebastian Ullrich (Jun 30 2025 at 08:59):

I can reproduce with the added step lake exe cache get between steps 2 and 3

Sebastian Ullrich (Jun 30 2025 at 09:27):

As far as I can tell, this is because leantar started skipping files that look up to date, but they only do so when looking at the githash and not the release string:

$ lean +4.21.0 --version
Lean (version 4.21.0, x86_64-unknown-linux-gnu, commit 6741444a63ee, Release)
$ lean +4.21.0-rc3 --version
Lean (version 4.21.0-rc3, x86_64-unknown-linux-gnu, commit 6741444a63ee, Release)

/cc @Mario Carneiro @Kim Morrison @Mac Malone - it's hard to say which component is even at fault here but I believe the best fix would be to ensure different releases are never created from the same commit; they create different .oleans after all.