commit convention

Stream: mathlib4

[Mario Carneiro]

PSA: The commit / PR title convention for mathlib4 is to use feat: desc/ chore: desc / refactor: desc / fix: desc. We no longer use feat(file/name): desc, if you want to include a file name then you should work it into the description. For port commits, my recommendation is feat: port Data.Nat.Basic.

[Ruben Van de Velde]

Mario Carneiro said:

PSA: The commit / PR title convention for mathlib4 is to use feat: desc/ chore: desc / refactor: desc / fix: desc. We no longer use feat(file/name): desc, if you want to include a file name then you should work it into the description. For port commits, my recommendation is feat: port Data.Nat.Basic.

I seem to have scrolled past this, so I'll bump it in case anyone else did as well

[Eric Wieser]

Sounds like something we could write CI for

[Sebastian Ullrich]

Been there, done that! https://github.com/leanprover/lean4/blob/master/.github/workflows/pr.yml

[Scott Morrison]

I'll move it to mathlib4

[Scott Morrison]

Oh, hmm, I don't like it, I think we need to be more flexible.

[Scott Morrison]

This should read the PR description, not look at any commit messages.

[Scott Morrison]

For mathlib(4), it is very common that people submit PRs with very complicated commit histories, particularly because it is common to branch off other open PRs to add further work.

[Scott Morrison]

And many contributors don't use rebase or squash at all.

[Eric Wieser]

If that CI runs on the bors batch it will be enough

[Eric Wieser]

It will rip the batches into little pieces if you're not careful, but it should at least do so instantly

[Scott Morrison]

But it's way too late to be complaining then.

[Scott Morrison]

Getting stuff through bors is already far too slow, we can't add anything that throws up delays at the last moment.