On Tue, Dec 14, 2021 at 1:32 PM David A. Wheeler <[email protected]> wrote:
> > > > 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. > This is what the *PR history* is for. These commits don't need to make it to master. > 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". > The history of a PR is less important when you are looking at master. When you use squash merge, the squashed commit contains a reference to the PR page, where you can see the blow by blow (and the associated discussion!) if you want to. > Git handles changes just fine without rebasing or squashing. It's > definitely not a hill to die on, > but I prefer avoiding both. > Git can handle it, but it's a lot more confusing for people looking at the history; things like HEAD~3 go who knows where and it's difficult to see at a glance what's going on when half of the commits are merges that clutter up the graph. -- 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/CAFXXJSsBM9Q%3DhHHkpLNkWDsgpnQmaNaYb5SidpuTfUswy2u-wQ%40mail.gmail.com.
