Merge conflict - localization

Stream: new members

[María Inés de Frutos Fernández]

PR #12081 has a merge conflict since it was modifying ring_theory/localization, which no longer exists. I think that the lemmas I added there should now go in ring_theory/localization/basic. I don't really now how to resolve this kind of merge conflict, should I just create a new PR adding the lemmas to the new file, and close PR #12081?

[Eric Rodriguez]

the way I went about this for my similar PRs was something like:

$ git switch master
$ git pull
$ git switch my_branch
$ git merge master
$ git rm src/ring_theory/localization.lean
(re-add all my changes manually in VSCode)
$ git commit

not sure if this is the best way

edit:added some extra steps

[María Inés de Frutos Fernández]

OK, I'll try this. Thanks!

[Anne Baanen]

I think your merge went wrong somehow, because GitHub claims 12 thousand new lines! I'll try and make a fixed branch

[Anne Baanen]

branch#is_localization_lemmas_merged

[Anne Baanen]

I followed Eric's steps (with a quick git diff at the start to see what I had to re-add)

[Eric Wieser]

I would recommend:

$ git fetch origin master
$ git merge origin/master

instead of what you suggested as git switch master; git pull; git switch my_branch; git merge master

[Eric Wieser]

I suspect the mess on the branch was caused by somehow doing the merge in the wrong direction

[Anne Baanen]

Wouldn't the following command then become git merge origin/master?

[Anne Baanen]

In any case, I'm happy to apply my new branch or you can do it with the following commands:

$ git fetch
$ git push origin 67258754ade8ef18882b8d39176dd684a7908748:refs/heads/is_localization_lemmas --force-with-lease

The first command downloads the latest commits from GitHub, the second command tells GitHub that the is_localization_lemmas branch should point to commit 67258754ade8ef18882b8d39176dd684a7908748 (which is the one I just pushed)

[Eric Wieser]

Anne Baanen said:

Wouldn't the following command then become git merge origin/master?

Yes, see my edit

[María Inés de Frutos Fernández]

Anne Baanen said:

In any case, I'm happy to apply my new branch or you can do it with the following commands:

$ git fetch
$ git push origin 67258754ade8ef18882b8d39176dd684a7908748:refs/heads/is_localization_lemmas --force-with-lease

The first command downloads the latest commits from GitHub, the second command tells GitHub that the is_localization_lemmas branch should point to commit 67258754ade8ef18882b8d39176dd684a7908748 (which is the one I just pushed)

Sorry, I just saw this. I have just pushed changes to my branch (adding my lemmas to the new files). Should I still do this now?

[Anne Baanen]

If you could push your changes, I can fix the merge and push the fixed versions to your branch

[Anne Baanen]

(Or is commit e744644705 already the last part?)

[María Inés de Frutos Fernández]

I just pushed the changes here. Is this what you mean? Other that this, the only file I have intentionally changed is field_theory/ratfunc, in this previous commit.

[María Inés de Frutos Fernández]

Yes, that commit is the last part.

[María Inés de Frutos Fernández]

Thank you! :smile:

[Anne Baanen]

Perfect, then I already got those changes. Shall I go ahead and push the fixed commits to your branch?

[María Inés de Frutos Fernández]

That would be great, thanks!

[Anne Baanen]

Done :+1:

[Anne Baanen]

Sorry, now it's done!

[Eric Rodriguez]

Eric Wieser said:

I would recommend:

$ git fetch origin master
$ git merge origin/master

instead of what you suggested as git switch master; git pull; git switch my_branch; git merge master

can you explain what the difference is, Eric? I should learn git better

[Anne Baanen]

Eric W.'s commands only update the remote tracking branch origin/master with git fetch, while Eric R.'s commands update the remote branches and also the local branch master with git pull. It's less work, so less commands to potentially mess up or forget.

[Eric Wieser]

Anne Baanen said:

Sorry, now it's done!

Watch out though @María Inés de Frutos Fernández, you'll need to run git fetch origin git reset --hard origin/yourbranchname (which throws away your local changes), otherwise next time you commit you're reintroduce the history mess

[Eric Wieser]

Anne Baanen said:

Eric W.'s commands only update the remote tracking branch origin/master with git fetch, while Eric R.'s commands update the remote branches and also the local branch master with git pull. It's less work, so less commands to potentially mess up or forget.

More importantly though, fetch doesn't touch your working tree and throw away changes you forgot to commit, unlike switch which I think might.