v4.24.0 tag

Stream: mathlib4

[Yaël Dillies]

@Kim Morrison, there is currently no v4.24.0 tag on mathlib. Are you aware of that? (I realise you bumped an hour ago, so maybe you're in the middle of doing it)

[Eric Wieser]

Maybe the goal is to add the deprecated modules first?

[Eric Wieser]

I don't think there's anyrequirement for v4.24.0 to tag the _first_ commit at that lean version

[Kim Morrison]

It's still in progress.

(For future reference, if you are ever concerned about the state of the release, you can run script/release_checklist.py v4.24.0 in the Lean4 repository. It will tell you the current state of things, and I won't post release announcements until it is all green --- and in particular, verifying these tags is on the checklist. :-)

[Kim Morrison]

But no, I wasn't planning on doing anything regarding deprecated modules. :-)

[Ruben Van de Velde]

I added all the missing deprecated modules yesterday