branch : “Can’t automatically merge.”

Stream: new members

[Antoine Chambert-Loir]

While working on branch#acl-Wielandt, GitHub complains that it can't automatically merge with master, and I would like to understand why / if this is a problem / what I need to do…
By the way, leanproject get-cache can't find an appropriate cache…

[Arthur Paulino]

When I tried git merge master on your branch it said:
CONFLICT (add/add): Merge conflict in src/group_theory/group_action/embedding.lean

It means that you added something that conflicts with something that someone else added

[Johan Commelin]

@Antoine Chambert-Loir This is a problem for github, but probably not for you. It just means that git thinks it would be good to have a human looking at the merge problem. But it doesn't mean the problem is hard.

What you should do:

git checkout master
git pull                        # get the latest stuff from master
git checkout acl-Wielandt
git pull                        # probably not needed, I guess you already have the latest stuff
git merge master                # ask git to merge
# now git will tell you that there are conflicts, and in which files
# fix the conflicts (e.g. in VScode)
# and follow the instructions that `git status` gives you

[Arthur Paulino]

When I open src/group_theory/group_action/embedding.lean I see:

<<<<<<< HEAD
This file provides a `mul_action G (α ↪ β)` instance that agrees with the `mul_action G (α → β)`
instances defined by `pi.mul_action`.
=======

This file provides a `mul_action G (α ↪ β)` instance that agrees with the `mul_action G (α → β)`
instances defined by `pi.mul_action`.

>>>>>>> master

[Johan Commelin]

So git is confused about whether you want those empty lines or not.

[Arthur Paulino]

You want to replace the whole <<<<<<< HEAD ... >>>>>>> master by the version you think is appropriate.

[Arthur Paulino]

I've never tried it, but apparently GitHub offers an interface to help you solve merge conflicts on your web browser:
https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/addressing-merge-conflicts/resolving-a-merge-conflict-on-github

It looks reasonably simple from what I can see. Very similar to what you'd have to do on your local text editor

[Arthur Paulino]

(The tutorial doesn't cover this very first step, but you'll need to open the PR)

[Arthur Paulino]

Should we add guidelines on how to deal with merge conflicts on the Pull request lifecycle page?

[Johan Commelin]

@Arthur Paulino I think it makes sense to at least include a mention (+ pointer on how to deal with them)

[Arthur Paulino]

Okay, I'm going to explain very briefly when it happens (1~2 lines max) and then link to that GitHub tutorial

[Antoine Chambert-Loir]

Thank you all for your help. And sorry to bring always my confusion here.
(The issue was that I had copied an early version of embedding.lean before it was PR'd by @Eric Wieser into mathlib.)

[Arthur Paulino]

Np. This community has always been of great help to resolve my confusions too

[Arthur Paulino]

@Johan Commelin https://github.com/leanprover-community/leanprover-community.github.io/pull/259

[Johan Commelin]

Thanks