language release notes cluttered by grind changes

Stream: general

[Edward van de Meent]

I've made it a habit to read Lean's release notes (specifically the language changes), and it keeps getting harder and harder to find changes to syntax and elaboration over the massive amount of changes to the grind tactic. I have no complaints about those improvements and changes themselves, but since i'm not interested in using grind for the forseeable future, reading the releasenotes to find changes i'm interested in is becoming increasingly difficult and time-consuming.
Because of this, i'd like to ask if it is possible to create a separate header or subheader for changes to grind, so people know where to start/stop reading, depending on their interests?

[Kim Morrison]

I would merge a PR modifying script/release_notes.py that took the changelog-lang section and sorted items there according to whether grind does not appear in the text or not, I guess.

[Eric Wieser]

Perhaps a less fragile mechanism for future releases would be a new changelog-lang-grind tag?

[Michael Rothgang]

I do like reading about grind improvements, but locating the non-grind changes is indeed tricky.

[Julian Berman]

The Mathlib commit log has a very minor similar issue where sometimes it feels like it'd be nice if there was a deliberate way to filter for "there's new math in this commit" rather than new linters or changes to underlying tactic functionality.

[Weiyi Wang]

Isn't that what "feat","chore"...prefixes are for?

[Chris Henson]

Weiyi Wang said:

Isn't that what "feat","chore"...prefixes are for?

These overlap with differentiating between roughly "infrastructure" and "new math" that I think Julian means.

[Kim Morrison]

Eric Wieser said:

Perhaps a less fragile mechanism for future releases would be a new changelog-lang-grind tag?

I'm unconvinced this is good use of anyone's time.

[Eric Wieser]

Maybe a better categorization would be changelog-tactics?

[Kim Morrison]

lean#10436

[Joachim Breitner]

We also have a volunteer, @Violetta Sim , who summarizes the changelog in the highlights. If someone wants to do a similar service to the community and group the release notes more sensibility, that could be a manual step as well. If someone reads them anyways completely, this may not be too unreasonable amount of work. It should probably only happen after the release, though, to avoid merge conflicts as further RCs come out.