Coq: Adopting a standard format for the CHANGES file?

[herbelin]

Version

Targetting 8.9.

Description of the problem

When adding a line to the CHANGES file, I'm always confused about which layout and style to adopt, about which head section to use, and various other questions. Could we try to adopt a common guideline?

Here are a couple of questions to start with:

• Length of lines?
• Use of `, or of ", or of [...], etc. to refer to Coq syntax?
• Skipping a line between items of a list or not?
• Use of capitals in acronyms, for instance ocaml, OCaml, ..., ascii, ASCII, ...? Do we adopt official spellings as much as possible? Do we prefer uniformity of style within the CHANGES file itself?
• Choice of headers? Should features be highlighted by having their own headers? Should features enter the category they belong too. We can take the "Display diffs between proof steps" feature as an example.
• do we assign someone the responsibility to check at the syntactic consistency of CHANGES? (I think I missed the discussion about whether CHANGES has an official maintainer or not.)

[Zimmi48]

I personally started using markdown-styled quoting in CHANGES in the hope that we would move at some point to a markdown file and that it would make transitioning easier.

I would approve having (short) guidelines on the style to use. These guidelines should be added to the contributing guide. It is not uncommon that contributing guides include such guidelines (and also how to write commit messages for instance).

Do we adopt official spellings as much as possible?

:+1:

Choice of headers?

IMHO we should have a standard set of headers that we reuse every time in the same order. This info could be documented in the release documentation (dev/doc/release-process.md) and it could be the role of the RM to create such (empty) sections just after branching.

I think I missed the discussion about whether CHANGES has an official maintainer or not.

There is no code owner to avoid spamming. I guess we can say it is the responsibility of the RM to check the consistency of CHANGES before a release.

[JasonGross]

I would support renaming CHANGES to CHANGES.md to get GitHub to render it more nicely.

[herbelin]

8151 shows a case of modification to CHANGES where both ` ... ` and [ ... ] are used. As a reviewer, do I recommend the author to use only ` ... `?

Is there someone who cares about the subject of the discussion and who did not express an opinion?

[Zimmi48]

I think that this is mostly solved now with the documentation at https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog.