HowToRebase - coq/coq GitHub Wiki

This page is about a seemingly common mistake people do when rebasing and how to avoid it. The mistake causes complicated commit histories and makes github produce silly commit numbers and diffs, and pings many unrelated codeowners.

TLDR: when pushing after a rebase if git tells you to git pull DO NOT do it, instead do git push -f.

Git graphs are as produced by git log --graph --oneline, so newer commits are at the top. When a commit is in a branch the branch is between brackets, eg deadbeef [master] commit message.

Starting state: we (branch1) made a commit based on 19ca577 but meanwhile something got merged into master. (foo conflicts in master vs branch1, but the issue will appear even without such conflicts. The conflict is just used to prompt us to rebase in the example scenario.)

014e5f4 *   [origin/master] merge branch2
        |\
d66f5c7 | * blob > foo
        |/
75c6c04 | * [origin/branch1] thing > foo
        |/
19ca577 * base

In branch1: git rebase origin/master, solve conflicts, git rebase continue

362d03f * [branch1] thing > foo
014e5f4 *   [origin/master] merge branch2
        |\
d66f5c7 | * blob > foo
        |/
75c6c04 | * [origin/branch1] thing > foo
        |/
19ca577 * base

git push says:

error: failed to push some refs to '/tmp/tmp'
hint: Updates were rejected because the tip of your current branch is behind
hint: its remote counterpart. Integrate the remote changes (e.g.
hint: 'git pull ...') before pushing again.

Here git is wrong, you don't want to "integrate" your old commits, instead you want to overwrite them with git push -f.

Let's see what happens if we git pull: git says

Automatic merge failed; fix conflicts and then commit the result.

Then after we fix conflicts and git commit we get

f0cb0d3 *   [branch1] Merge branch 'branch1' of origin into branch1
        |\
75c6c04 | * [origin/branch1] thing > foo
362d03f * | thing > foo
014e5f4 * |   [origin/master] merge branch2
        |\ \
        | |/
        |/|
d66f5c7 | * blob > foo
        |/
19ca577 * base

(now git push works and puts this strange graph on your remote repository)

So merging the resulting branch1 to master would add the following commits to master:

362d03f thing > foo (non rebased)
75c6c04 thing > foo (rebased)
f0cb0d3 merge branch1 into branch1

It seems that if we make a PR from branch1 to master github will also think "d66f5c7 blob > foo" is included too for some reason. Since in the general case we can rebase over an arbitrary number of commits instead of the single blob > foo commit this produces the large commit numbers, diffs and codeowners mentioned at the start of this page.