doc or docs? Consistency in commit messages

Stream: mathlib4

[Kevin Buzzard]

buzzard@buster:~/lean-projects/mathlib$ git log | grep "docs(" | wc
     42     279    2955
buzzard@buster:~/lean-projects/mathlib$ git log | grep "doc(" | wc
    121     769    8381
buzzard@buster:~/lean-projects/mathlib$

Apparently 42 mathlib commits are of the form docs(Computability/NFA) (#6467) and 121 are of the form doc(Topology/Homeomorph): two docstrings (#7595). Do we care about sticking to one convention for commit messages, and if so can we get CI to check for it?

[Julian Berman]

(https://github.com/conventional-changelog/commitlint is a widely used commit linter if the answer is someone cares. It doesn't do anything to retroactively 'fix' anything existing clearly.)

[Damiano Testa]

I thought that there was a CI step that checked something about how PR names begun, but maybe it is not on Mathlib, but on a dependency?

[Damiano Testa]

Ah, it is core itself that has this: https://github.com/leanprover/lean4/blob/master/.github/workflows/pr-title.yml.

[Ruben Van de Velde]

I'd already be happy if we managed to update the commit message when we change what a pr is doing :)

[Damiano Testa]

Now that there is a little bit of automation around summarizing PRs, it may be a fun experiment to see whether a bot can categorise PRs as feat, doc, or chore.

[Damiano Testa]

Just looking at the change in declarations may already give a good heuristic.

[Kevin Buzzard]

I was wondering about something far more basic -- checking whether the commit message began with one of the allowable strings, rather than guessing which one

[Damiano Testa]

Yes, I think that the CI step that I linked to above does exactly that, for core.

[Michael Rothgang]

Kevin Buzzard said:

I was wondering about something far more basic -- checking whether the commit message began with one of the allowable strings, rather than guessing which one

#16303 does that (and more --- I'm happy to extract just that subset, if desired). At the moment, it's not so clear to me if the PR is considered useful, so your opinion is valuable!