Rebase vs merge

Stream: mathlib4

[Alfredo Moreira-Rosa]

If i may, merging master to branches can also trigger issues because you get a graph loop, and if the PR gets open for a long period, and you merged master back many times, when you'll really merge to master, you can get really hard to fix merge conflicts.
So my personnal advice is (if you can), rebase from master (git rebase) instead of merging master back.

[Ruben Van de Velde]

What?

[Ruben Van de Velde]

I would not recommend rebase to anybody who doesn't already know what it is

[Weiyi Wang]

:sweat_smile:In some project culture like the previous one I was in, developers like to recommend git rebase, but yeah I agree you have higher chance of messing up there if you don't know what it does

[Alfredo Moreira-Rosa]

i may be biaised, but i'm so used to rebasing that i do it as fast as merges.

[Ruben Van de Velde]

Sure, but I'm explicitly not talking about you

[Yakov Pechersky]

Since Mathlib is managed via bors, which is an approach of staged squash and merge of individual PRs, rebase doesn't work so well since the squash is an independent commit.

[Yakov Pechersky]

Additionally, stepping through the rebase one conflicted commit at a time fixing proofs can be repetitive and self defeating if a later commit performed yet another refactor or move or something would require more fixes.

[Notification Bot]

8 messages were moved here from #mathlib4 > CI failure by Ruben Van de Velde.

[Jovan Gerbscheid]

Also, the github PR history is nicely preserved when merging master (and not rebasing)

[Eric Wieser]

ecyrbe said:

you merged master back many times, when you'll really merge to master, you can get really hard to fix merge conflicts.

I've never seen this behavior; if you merge master many times as you go along, the conflicts are likely to be much easier to solve, not harder.

[Eric Wieser]

Things go wrong if you mix this strategy with rebasing

[Alfredo Moreira-Rosa]

yes, when you rebase, you have to always rebase. not mix with merge back.

[Eric Wieser]

https://github.com/mhagger/git-imerge can be quite handy for dealing with nontrivial conflicts

[Alfredo Moreira-Rosa]

Jovan Gerbscheid said:

Also, the github PR history is nicely preserved when merging master (and not rebasing)

you can rebase without squash. (squash = rebase -i ; basic rebase = git pull --rebase)

[Eric Wieser]

But that's not the actual history, that's a retelling of the history; especially if each commit has merge conflicts that are resolved manually.

[Yakov Pechersky]

For Mathlib, I've found rerere super useful. Especially when I'm updating a lot of branches by a merge master.