notes for adaptations each release cycle

Stream: mathlib4

[Matthew Ballard]

Would it be useful to write down in a centralized place what major stylistic changes were made to mathlib when bumping to the next Lean release?

For example, someone is upgrading their own work to v4.7.0 and they don’t know why simp is broken or what to do. Pointing them to a document summarizing changes like “find all let’s and explicitly include them” might save some time.

[Kevin Buzzard]

With the chaos that is happening behind the scenes trying to keep mathlib up to date, I'm secretly really glad I haven't started seriously on FLT yet.

[Johan Commelin]

The commit message should contain all that info, but we could consider all listing it in another place.

[Matthew Ballard]

One could also argue that this for the Lean release notes (assuming it is not specific to mathlib)