merging or squash merging?

Stream: mathlib4

[Thomas Murrills]

When we merge from master into a feature branch, is it ok to squash merge? (Sometimes there are hundreds of commits.) I'm just checking to make sure squash merging won't somehow break anything when the feature branch is eventually merged into master.

[Thomas Murrills]

(In general I would rebase, but in PR's where the convention seems to be to merge from master, I figure it's cleaner there to keep merging—right?)

[Patrick Stevens]

PRs tend not to use rebase because rewriting the history of a commit that someone else might be working with (e.g. if they've pulled the branch) will make their life a lot harder when they come to sync again. Notice that updating a branch by rebasing will require you to force-push the rebased commit (unless you do some shenanigans like manually creating the tip commit with multiple parents, I guess, but I don't think anyone ever does that), which is usually a good indicator that you're about to break anyone else who was relying on the commits you're "overwriting".

[Patrick Stevens]

I would expect squash-merging master to be liable to break your own future merges of master, because a squash-merge of master will not actually merge any commit from master into your branch - only construct a new commit whose contents are the same as master's. I would expect Git's three-way merge to sometimes be unable to find appropriate base commits to perform the next merge against.

[Patrick Stevens]

Is there a reason other than aesthetics for not simply doing an ordinary merge? Note that GitHub will usually show history in a sane way when you merge master - that is, it will just show a single merge commit but will prioritise showing reviewers commits from your branch. It's only when parts of history were squashed that it resorts to showing individual commits from master on your pull request. Do you have a case where it didn't?

[Eric Wieser]

git merge --squash origin/master is almost always a really bad idea

[Eric Wieser]

You should only ever use git merge --squash A-branch-I-will-never-need-again

[Eric Wieser]

Squash merging master means "take all the changes that happened on master and create a new commit containing them on my branch with no reference to the commit I merged, so that now I have merge conflicts with files my PR barely even touched"

[Floris van Doorn]

I definitely sometimes rebase a PR onto master (or squash a bunch of my branch commits into a single commit). I only do this if it has not had any reviews yet. If there are reviews, it's nice to keep the context when the comments were made.

[Eric Wieser]

Rebasing a PR onto master is indeed fine in many scenarios, but squash merging master into a PR is always wrong. Squash merging a PR into a local copy of master is just "Rebasing a PR onto master" with extra steps.