> On Dec 14, 2021, at 12:51 PM, Mario Carneiro <[email protected]> wrote:
>
>
>
> On Tue, Dec 14, 2021 at 12:47 PM Mario Carneiro <[email protected]> wrote:
> One thing that I think we should stick to is one commit per PR. We had a
> similar discussion for metamath-knife but for set.mm it's important to keep
> PR sizes down so that people can reasonably review them, and squash merges
> keep things organized. This is the mechanism we've been using in mathlib and
> it works well to avoid merge conflicts, especially when things scale to many
> concurrent PRs.
I think multiple *commits* per PR is fine, especially if the later commits are
small changes that fix the initial commit based on feedback. Then it's clear
that comments were acted on.
I think the more important rule is that every logical change should be a
separate PR.
Some PRs will be accepted, others not, and we don't want to lose good idea #1
if idea #2 is rejected.
> For big PRs that benefit from multiple commits, I think the commits should be
> consciously organized, squashing away bugfix commits and rebasing (not
> merging) on master. Such PRs are merged using the "rebase" option instead of
> "squash", but "squash" should be the default (and "merge" should not be used).
Squashing & rebasing instead of merging is the latest fashion. I'm not a fan of
these bell bottomed pants.
Squashing eliminates the history of what actually happened, in particular, it's
hard to tell
if an earlier comment was acted on if you eliminate the history through
squashing.
You also can't tell what "really happened".
Git handles changes just fine without rebasing or squashing. It's definitely
not a hill to die on,
but I prefer avoiding both.
--- David A. Wheeler
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/8E6B5E47-7D97-49CE-B6E7-B2E644EE5756%40dwheeler.com.
