v4.23.0

Stream: general

[Kim Morrison]

This thread can be used for discussion of the new v4.23.0-rc2 release.

[Eric Wieser]

From #announce > v4.23.0-rc2 @ 💬

[Eric Wieser]

nit: lean4#9106 was backported, so perhaps belongs in the 4.22.0 release notes and not these ones

[Geoffrey Irving]

Does @[unbox] work yet, or is that planned for a later release? When I last asked (a good while ago) it was waiting on the new code generator, but now that’s in.

[David Renshaw]

grind regression: the following proof works in v4.22.0 and not in v4.23.0-rc2. (increasing the splits threshold does not help`)

theorem foo (k m : Nat) (c : Nat → Nat)
    (hk₀ : k ≤ m)
    (h₅₀ : ∀ (a b : Nat), c a - c b = (a - b) * (a + b + 1))
    (x : Nat) : c k ≤ c (m + x) := by
  grind

edit: fixed apparently

[Henrik Böving]

Geoffrey Irving said:

Does @[unbox] work yet, or is that planned for a later release? When I last asked (a good while ago) it was waiting on the new code generator, but now that’s in.

It doesn't work yet

[Yaël Dillies]

Is it expected that the release notes contain what seems to be the first line of a code snippet, but not the rest?
image.png

[Yaël Dillies]

In fact, there are many many such truncated code snippets. I suspect there's something wrong with the PR description extraction

[Jireh Loreaux]

Kim Morrison said:

We'd like to highlight the benchmarking results for the commit that moved Mathlib to v4.23.0-rc2, which is a sea of green (including a 15% instruction count reduction overall).

Do we have any idea which changes to core are primarily responsible for this speed-up?

[Yaël Dillies]

It looks we know which changes to core made core faster, and one could extrapolate that the same changes might be the ones that sped mathlib up. But we can't know for sure since each individual change wasn't benchmarked against mathlib

[Jireh Loreaux]

Sure, I understand we can't know for sure, I'm just looking for suspected culprits.

[Kevin Buzzard]

Someone needs to check that the commit after wasn't a sea of red :-) The speedcenter has been very noisy over the last couple of months.

[Jireh Loreaux]

It's normal, I checked. The speedcenter has been noisy, but not 15% noisy across Mathlib.

[Michael MacLeod]

Thank you to whoever made it so that jump to definition on typeclass functions also shows the instance's definition. Super helpful.

[Kim Morrison]

That's @Marc Huisinga to thank! It's pretty lovely, isn't it?