Zulip Chat Archive

Stream: new members

Topic: git help

Winston Yin (Jun 13 2021 at 08:01):

I'm following the instructions on how to make a PR, and I'm getting stuck at git push origin. It says I need to first git pull, but that just introduced a bunch of merge conflicts that have nothing to do with me

Winston Yin (Jun 13 2021 at 08:03):

What I've done: leanproject get -b mathlib:representation, moved a single new file into src, then staged it and git commit -a. Then git pull --set-upstream origin representation gave me a list of merge conflicts

Winston Yin (Jun 13 2021 at 08:04):

One such line:

CONFLICT (modify/delete): src/algebra/module.lean deleted in HEAD and modified in 52a6ca3fff2b497fb409b037ec8193f7d09fc86f. Version 52a6ca3fff2b497fb409b037ec8193f7d09fc86f of src/algebra/module.lean left in tree.

Winston Yin (Jun 13 2021 at 08:16):

I've "accepted all incoming" and pushed. This is the commit: https://github.com/leanprover-community/mathlib/commit/9215e39164877100d8bac41d0a7c241bb75a2cb9

Winston Yin (Jun 13 2021 at 08:17):

The commit contains the file I added: representation.lean, but also a bunch of other files I never touched. Please let me know if I'm doing this wrong and messed something up.

Eric Wieser (Jun 13 2021 at 08:18):

does branch#representation already exist?

Winston Yin (Jun 13 2021 at 08:23):

Yes, I think that's the issue. It seems I've pushed my commits to that branch. How can I fix this?

Winston Yin (Jun 13 2021 at 08:24):

I'm sorry. I'm still learning git and may have messed things up here

Eric Wieser (Jun 13 2021 at 08:28):

You should pick a new branch name and use that instead

Eric Wieser (Jun 13 2021 at 08:32):

Then I guess @Scott Morrison can clean up whatever mess you might have made of their branch

Eric Wieser (Jun 13 2021 at 08:33):

It's often a good idea on mathlib to use yourusername/yourtopic as the branch name to stop this type of thing happening

Winston Yin (Jun 13 2021 at 08:33):

I'll make a new branch with my name

Winston Yin (Jun 13 2021 at 08:33):

Sorry @Scott Morrison

Last updated: Dec 20 2023 at 11:08 UTC