v4.12.0 discussion

Stream: general

[Ruben Van de Velde]

@Kim Morrison lake doesn't seem to find a v4.12.0 tag on mathlib, are you sure it's there?

[Kim Morrison]

Oops, adding now.

[Kim Morrison]

Mathlib is always a pain because it takes an hour for the PR to land, and then I forget to tag it... :woman_facepalming:

[Kim Morrison]

Should be there now.

[Eric Wieser]

Is a v4.12.1 release likely, fixing the regression in lean4#5565?

[Asei Inoue]

very nice! good release!! :tada:

[Kim Morrison]

Eric Wieser said:

Is a v4.12.1 release likely, fixing the regression in lean4#5565?

Sorry, that hadn't been on my radar. Seems plausible. Is it a blocker for anyone at present?

[Eric Wieser]

I think it's mainly a usability/performance issue, though also it might allow ignored timeouts to sneak into mathlib which become annoying to resolve later

[Eric Wieser]

One other regression in (mathlib) v4.12.0:

Eric Wieser said:

In Lean 4.12.0, the instance docs#List.decidableInfix looks to have been deleted accidentally when bumping mathlib.

Fixed in #17420, but I guess this won't help with the stable v4.12.0 release of mathlib.