lean4 PR conventions

Stream: lean4 dev

[Joachim Breitner]

<https://github.com/leanprover/lean4/blob/master/doc/contributions.md> is a good start, but it still left some questions open for me, in particular

• should PR branches have a clean, curated commit history, or a honest, chronological one
• will merges happen as squash or no-ff merges
• where does the commit message come from.

Empirically, it seems that

• PR commit history doesn’t matter and can be honest, chronological
• PRs are merged as squash merges
• Commit message titles are taken from the PR title, and no body.

The first two of these happen to match my preferred workflow (messy, honest commit history on branches, no rebases, squash-merged for a cleaner master history).
The last one makes me wonder if that’s just the path of least resistance when manually merging, or is it an intentional choice?
(Personally, I like it when the final commit message is taken from the PR description, or a part of it, just like in mathlib).

Once confirmed by the devs, I am happy to update the documentation to clarify these points. And cross-link with <https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md> and <https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md>.

Or is this all in flux anyways and the introduction of some form of automerging (like bors or mergify) is planned soon?

[Scott Morrison]

I think in practice the current rule is that PRs can be merged either as a curated history with multiple commits, or as a squash merge.

For now, all PRs from external contributors are being squash merged (as the path of least resistance), although I think it would be fine if a contributor explicitly stated they wanted commits preserved.

I agree we should make this clearer and simpler!

[Mario Carneiro]

Note that PRs that include an update-stage0 cannot be squash merged

[Leonardo de Moura]

For now, all PRs from external contributors are being squash merged (as the path of least resistance), although I think it would be fine if a contributor explicitly stated they wanted commits preserved.

I only squash external PRs when the commits are not following our naming conventions or are messy (e.g., there is a commit that reverts a change made in the same PR).

[Sebastian Ullrich]

For the contribution guidelines, it should be sufficient to say that at the end of the review cycle, PRs should have a well-structured commit history conforming to the commit message conventions. We can still squash-merge (or ask for improving the history) when that's not the case.

[Sebastian Ullrich]

Joachim Breitner said:

Or is this all in flux anyways and the introduction of some form of automerging (like bors or mergify) is planned soon?

I don't think it will be affected by that

[Joachim Breitner]

I see, a “smart merge” strategy :-)

My preference is to not bother with clean commit messages on branches (it's busywork, and hard to review/edit) and instead require good _PR_ descriptions (much more prominent, easier to edit by all parties), and use squash merge by default using the PR title/description.

This has the additional benefit that there is no need to rebase/force push feature branches. Force pushing makes it harder to see what happened (GitHub's infamous “cant find this commit” instead of nicely showing the differences) and harder to juggle multiple feature branches. And as a reviewer I find it easier to follow if a new “fix typo and add EOL at EOF” commit shows up, rather than a unlabeled force push that could have changed anything.

[Scott Morrison]

This is my preference too, but I have sometimes erred too far on the side of messy git histories on Mathlib!

[Joachim Breitner]

How can it be too far? Once the PR is squash-merged, the branch git history is, eh, history :-)

[Scott Morrison]

When the list of commits starts obscuring everything else on the github PR page, you've gone too far. I have since got better at rebasing.

[Eric Wieser]

In mathlib3 rebasing was very undesirable because leanproject get-cache couldn't understand it (it resulted in discarding all the caches from your PR branch). That's now fixed with lake exe cache get which is content-addressed not git-hash-addressed.

[Mac Malone]

Joachim Breitner said:

This has the additional benefit that there is no need to rebase/force push feature branches. Force pushing makes it harder to see what happened (GitHub's infamous “cant find this commit” instead of nicely showing the differences)

I use rebasing/force pushing specifically to hide / make it hard to see the development process. I like presenting a crisp concise view of what was changed to the public by a logical grouping of commits rather than a messy debug log. But then again, maybe that just implies that I care too much about my appearance? :mirror: :laughing:

[Joachim Breitner]

Maybe … I fully understand that the appeal of providing a super polished commit sequence, have done that before. But is it really worth the effort? By squash-merging by default the incentive to spend time on branch appearance is maybe reduce, which is maybe a good thing?
(Of course, I don't mind polished branches, especially not before the first review, but I wouldn't require onr expect it.)
And in cases where a feature can really be turned into independent steps, separate PRs are probably preferable anyways?

[Mac Malone]

Joachim Breitner said:

separate PRs are probably preferable anyways?

This is definitely true for external contributions from the maintainers' perspective (and thus should likely be enforced there). As a regular developer PR to my own code, though, separate feature branches can require a lot switch back and forth and resolving merge conflicts as they grow independently. Also, it can require more work to extract the separate features coherently into separate PRs (since there maybe be independence even with logical separation in goal).

Joachim Breitner said:

Maybe … I fully understand that the appeal of providing a super polished commit sequence, have done that before. But is it really worth the effort?

For me, I find git add . && git commit --no-edit --amend && git push --force to be an easily replayed command when making logically related fixes and it does not require a mental break to come up with a commit message. But I suspect that is just preference.

[Joachim Breitner]

Good points. PRing your own code might certainly require a different workflow.