v4.20.0

Stream: general

[Kim Morrison]

Note that we had several problems with the intermediate release candidates, and v4.20.0-rc5 is the preferred release candidate.

[Kim Morrison]

Due to some time restrictions this week (the Lean FRO has been at our annual retreat), some of the repositories upstream of Mathlib do not yet have tags for v4.20.0-rc5, and are still on an earlier release candidates (and similarly their most recent tag may be for an earlier release candidate). This shouldn't be a problem, as the release candidates should only differ in user interaction and/or linking behaviour. If I have time I'll try to bring everything uniformly to v4.20.0-rc5, but I'd also welcome help doing this in places where people see the need. Running script/release_checklist.py v4.20.0-rc5 in the lean4 repository may be helpful!

[Shreyas Srinivas]

The release notes link points to the notes for rc3

[Kim Morrison]

(i.e. yes, and I'm not intending to update until we release the stable)

[Jared green]

(deleted)

[Pietro Monticone]

I opened the relevant doc-gen4 bump PRs so we can bump and tag FLT (FLT#476), but there’s no particular hurry.