Fsharp: I am going to start using Squash and Merge

[KevinRansom]

When committing F# PR's I think it will improve the quality of the history.

Comments?

[forki]

+1

[ploeh]

Please don't. It changes the history of the commits, not to mention their identity. Worse, it means that pull request branches look orphaned when fetching from upstream, causing unnecessary clean-up work on the contributor's part.

The repository history is what it is. How will it be improved by being manipulated?

[KevinRansom]

@ploeh There are a ton of commits in history that are just incidental happenstances. In reality the only significant commits are the one for the pull request, the others just map to how the developer happened parcel up the work.

Since I have moved to using Git it seems to me that the history is only usefull on my local branch for the few things I am currently working on. For sure when we used TFS internally, the history was a significant event.

For example:
https://github.com/Microsoft/visualfsharp/commit/794a3c48de8db147e4c888e907564cad82c5ab43

It would be fair to say, that I have no idea what PR this was feedback to. we would probably both agree that I should provide better commit comments ... yes but having to write a decent commit comment once for each PR must be preferable to write a novel for each commit in the PR.

Make sense or am I mistaken?

Kevin

[bikallem]

+1 for squash and Merge.

[moodmosaic]

What @ploeh wrote.

-1 for squash and merge.

[baronfel]

I'm lately in favor of rebasing feature branches into one or two worthwhile commits before merging them into master. Make the commit history meaningful instead of noise from needlessly reincorporating master prior to work being completed. Git encourages you to be commit often and messily on your local and feature work, but gives you the tools to clean it up before finalizing.

[forki]

@ploeh this project has historically always created strange looking histories. We discussed this multiple times and always the "we need to do it like ms does it" card was played. Many people disagreed with that practice.
In recent times things changed and real merges happened (without a official change of merging strategy). I personally was a big fan of this recent development.

My +1 is basically for changing the official strategy to something where PR and commit are still bound together (like Kevin already did for a couple of months). Tbh I don't really have a opinion if squashing is needed, but I learned that identity with git commits is just not that important. We cherry pick hundreds times a day at our company and somehow this all kind of works. ;-)

[forki]

I forgot to say: we should always encourage people to rebase their PRs before merging....

[enricosada]

I am in favor of squash as improvement, because a pr is a work in progress (review->feedback->fix->..) and i really think should be rebased and squashed to few commits before merge, leaving only some meaningful commits with identity (main work, a special use case, a workaround to easy revert, etc)
Rebasing a github pr doesnt lose review comments anymore, that was a big issue, now is ok.

Also github rebase+squash help improve the commit message, so it's nice for history

Squashed from github doesnt lose the connection to pr history an example so i think is ok.

What i'd really like to see is a rule to rebase pr before merge if possibile (if not too complicated).
Rebasing a pr make a history really simple, atm lot of times is just complicated because merge from master.
For example there are lots of pr with really small diff and some merge commit, that's annoying.

[dsyme]

I'm generally in favour of squashing

[KevinRansom]

Thanks for all of the feedback,

Conclusion:

• We will use merge/squash where we can from now on.
• There is no need to rebase, just carry on as now.
• Try to make sure
• Note:
  if a PR contains contributions from more than one contributor please note it in the PR description, we will use regular merge ... so everyone gets appropriate contribution credit. However, if I mess up from time to time please don't bash on me too hard :-)

From GitHub documentation: https://help.github.com/articles/about-pull-request-merges/

Note: When a pull request is merged and commits are squashed, only the user that merged the pull request and the user that opened the pull request receive contributions. No other contributors to the pull request will receive contribution credit.