how to resolve conflicts without messing up branch?

Stream: general

[Kevin Buzzard]

tl;dr: what's the best way to fix a conflict in a PR which depended on another, now merged, PR, without github becoming convinced that I just changed 200 files?

The details: I made a PR #14155 which depended on #13294 (which added a new file) . The depended-on PR #13294 is now merged, but changes were made to it during review. My PR also added one lemma to this file. I now need to merge master. I may or may not have typed some command a long time ago on this computer which says "always use the following strategy for merges" and, if I did, I don't know which strategy I chose (indeed I don't really understand what the difference between the various options is, and don't really care enough about the details to learn, I've read it before and it goes in one ear and out the other, this is beyond my git capabilities and interests). Usually things work out fine here but the last time I tried something like this (#13703) I ended up with my PR changing 800+ files and I had to close it and open a new one (#14176). Usually I would just do the same this time (i.e. give it a go, see if it works, and if it doesn't work then just close the PR and open a new one and move on with my life) but I noticed that the last time I did this I managed to pollute many other PRs with the message that I pushed a commit that referenced the PR, and I don't want to do this again if I can help it.

a) How do I avoid this?
b) If I fail to avoid it, Is there a way where I can check that what I'm about to push to github doesn't trigger this kind of mess? Or a warning sign which I can spot before doing it? Or a way of easily undoing it if I manage to do it again, hopefully without polluting many other PRs?

[Edward van de Meent]

i'm not a git-expert, but i believe that for fixing this situation, the keyword (and git command) you're looking for is rebase. i don't know the precise options that would be best suited to your case, but that should at least give you a place to start looking

[Edward van de Meent]

from memory, git rebase is a command that allows you to put the changes made from the last common commit with some branch, on top of the current head of that branch...

[Ruben Van de Velde]

Note that rebase is exactly the command that risks including lots of commits like that

[Ruben Van de Velde]

As far as I'm aware, merge won't cause that

[Ruben Van de Velde]

I can also just do it for you if you like, @Kevin Buzzard

[Richard Osborn]

Yes. Avoid rebasing when merging with a branch with squash merges. You could do git merge --no-ff --strategy=ort master to make sure your settings aren't secretly rebasing things (although, I don't think they should).

[Richard Osborn]

Here's the git FAQ pertaining to this issue.

[Damiano Testa]

I also find git diff --name-only master...HEAD very useful to find out which files git thinks that I have modified.

[Damiano Testa]

If the output of that is 800 files, chances are that something went wrong.

[Richard Osborn]

Also, make sure you aren't defaulting to git pull --rebase.

[Kevin Buzzard]

How? git config -l gives me a lot of output. What am I to make of this?

$ git config -l
user.email=k.buzzard@imperial.ac.uk
user.name=Kevin Buzzard
credential.https://github.com.helper=
credential.https://github.com.helper=!/usr/bin/gh auth git-credential
credential.https://gist.github.com.helper=
credential.https://gist.github.com.helper=!/usr/bin/gh auth git-credential
init.defaultbranch=main
core.repositoryformatversion=0
core.filemode=true
core.bare=false
core.logallrefupdates=true
remote.origin.url=git@github.com:leanprover-community/mathlib4.git
remote.origin.fetch=+refs/heads/*:refs/remotes/origin/*
pull.rebase=true
branch.master.remote=origin
branch.master.merge=refs/heads/master
branch.AK_unfolding_trick.remote=origin
branch.AK_unfolding_trick.merge=refs/heads/AK_unfolding_trick
branch.kbuzzard-group-cohomology-speedup.remote=origin
branch.kbuzzard-group-cohomology-speedup.merge=refs/heads/kbuzzard-group-cohomology-speedup
branch.hairer.remote=origin
branch.hairer.merge=refs/heads/hairer
branch.kbuzzard-coalgebra-refactor.vscode-merge-base=origin/master
branch.kbuzzard-squeeze-dsimp.vscode-merge-base=origin/master
branch.kbuzzard-pointwise-tinkering.vscode-merge-base=origin/master
branch.kbuzzard-pointwise-tinkering.remote=origin
branch.kbuzzard-pointwise-tinkering.merge=refs/heads/kbuzzard-pointwise-tinkering
branch.eric-wieser/pointwiseMulSemiringAction.remote=origin
branch.eric-wieser/pointwiseMulSemiringAction.merge=refs/heads/eric-wieser/pointwiseMulSemiringAction
branch.fiberedcategories_homlift.remote=origin
...

[Kevin Buzzard]

Right now I am completely confused because when merging the branches I found theorems in the file Eric added which as far as I can see were not added in either my branch or his :-)

[Kevin Buzzard]

Somehow I feel like this is something I need to learn how to do properly (I had not understood that it was the squash merge that was causing the problem) so I feel like I should persevere.

[Eric Wieser]

What you're running into here is a limiation of bors

[Eric Wieser]

Maybe we should have a wiki page for this

[Ruben Van de Velde]

Ah, pull.rebase=true

[Kevin Buzzard]

So this perhaps explains why the last time I tried this on this computer it was a catastrophe?

[Ruben Van de Velde]

Yes, I think it might

[Kevin Buzzard]

I'll try on another computer :-)

[Kevin Buzzard]

So indeed, exactly the same sequence of commands had a different result on the other computer and I have managed to merge without screwing up the PR. Yikes, git is so complex. Thanks to all!

[Kevin Buzzard]

If someone wants to tell me how to replace pull.rebase=true with whatever it should say, that would be great :-) This is way beyond my capabilities, I'm only finding commands like git config through google and I don't really like doing stuff like that.

[Ruben Van de Velde]

I think git config --unset pull.rebase will do it

[Eric Wieser]

Eric Wieser said:

Maybe we should have a wiki page for this

https://github.com/leanprover-community/mathlib4/wiki/Working-with-dependent-PRs is the start of my draft, with picture but no commands

[Floris van Doorn]

git merge origin/master -X theirs is the command "merge and choose their version whenever there is a conflict" (replace "theirs" by "ours" for the dual).

[Floris van Doorn]

Note that for git rebase the meaning of "ours" and "theirs" is flipped, for some very stupid reasons.

[Floris van Doorn]

My post here (and Yury's post above it) probably complements your draft well, because it contains the commands, but little explanation. Feel free to incorporate them.

[Floris van Doorn]

I do not recommend approach 2. You can do it, but personally I only know how to do it with interactive rebases, and then you have to make sure you keep the right files in your rebase.
But the main reason I don't like rebases is that when you've solved a merge conflict in an earlier merge/rebase, I believe you're likely having to do it again in a new rebase? That is my memory at least, but maybe I did something stupid. Merges are nicer in any case.

[Floris van Doorn]

But nice draft, that will be useful to have in a central location!

[Eric Wieser]

Floris van Doorn said:

git merge origin/master -X theirs is the command "merge and choose their version whenever there is a conflict" (replace "theirs" by "ours" for the dual).

I think in the context of this draft this is the wrong thing to do: you don't want "use their version whenever there is a conflict", you want plain "use their version in its entirety"

[Eric Wieser]

One reason to prefer approach 2 is that approach 1 leads to bad author information from bors if the base PR has a different author

[Eric Wieser]

But I agree that approach 1 is usually the safer bet

[Kevin Buzzard]

Is there a way of reliably recreating the deleted branch in our set-up? When I switched computers I tried first using my local copy of the deleted branch but it wasn't up to date, and then I tried updating it from origin but of course it was gone, and then I gave up and merged and manually fixed conflicts.

[Shreyas Srinivas]

For reference, I ran into this issue twice in the last 1.5 months. The least techie but slightly tedious way to get rid of the additional commits is to git reset --hard <ID of the last you made before catastrophe>. You can find this ID by opening git log and scrolling down to your commit. There are faster ways to narrow this hunt depending on the situation. Then you run git config pull.rebase false followed by git merge master. Then to get all of this to GitHub git push --force origin <your PR branch name>

[Shreyas Srinivas]

That should tidy up your PR

[Shreyas Srinivas]

To hunt through the logs you can also use the git graph vscode extension

[Shreyas Srinivas]

You can do everything I mentioned above within git graph's GUI

[Shreyas Srinivas]

Except the git config part, but that's a one time thing

[Eric Wieser]

Kevin Buzzard said:

Is there a way of reliably recreating the deleted branch in our set-up? When I switched computers I tried first using my local copy of the deleted branch but it wasn't up to date, and then I tried updating it from origin but of course it was gone, and then I gave up and merged and manually fixed conflicts.

Yes, you can pull it from the github UI

[Eric Wieser]

git fetch origin thehashfromthegithubui

[Kevin Buzzard]

Even if it tidies up the PR, does the force push method still pollute everyone else's PR?

[Shreyas Srinivas]

Nope

[Eric Wieser]

Force push is only the right choice here if you screwed up the merge, pushed, and realized you created a disaster

[Shreyas Srinivas]

I highly recommend the git graph extension if you want to play around with branches.

[Eric Wieser]

Or get used to git log --decorate --oneline --graph

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

This is the extension I am talking about: https://marketplace.visualstudio.com/items?itemName=mhutchie.git-graph

[Kevin Buzzard]

Damiano Testa said:

I also find git diff --name-only master...HEAD very useful to find out which files git thinks that I have modified.

This is a very useful comment as far as I am concerned. Can I just clarify: is "the files git thinks that I have modified" equal to "the files which github thinks that I have modified"? I'm still a bit unclear about precisely what is git and what is github.

[Julian Berman]

No unfortunately not, what the GitHub UI shows in e.g. its diffs can essentially be a black box at times and suffers from strange caching bugs in situations which are hard to reproduce and report to them.

[Julian Berman]

Personally I generally never trust the GitHub UI if its showing something different than what git seems to suggest what will happen, but obviously that's not a great thing when a reviewer is going to likely look at what's seen in the GitHub UI.

[Damiano Testa]

While what Julian said is correct, I have found it fairly reliable.

The main difference of course is that the command-line argument above reports information about the repository on your machine, while the GitHub webpage is based on what has been pushed. So, my comment made the distinction

• git -- what you have on your machine
• github -- what has been pushed to the remote repository.

[Damiano Testa]

So, e.g., if your PR on GitHub shows one modified line, since you removed an extra space, locally on your machine you merge master and the command above shows 275 modified files, very likely something has gone wrong somewhere.