Git merge problem

Stream: new members

[Josha Dekker]

I think that I've done something wrong on the branch underlying #9108. Last time I tried "fixing" a problem, I made it worse, so I thought I'd ask for input early on. I basically only incorporated the comment that urkud wrote, but when trying to commit in VS Code, I see "Sync changes 66 down, 2 up". Hitting the button, I get the following error message:

> git pull --tags origin JADekker_lindelof_spaces
From https://github.com/leanprover-community/mathlib4
 * branch                  JADekker_lindelof_spaces -> FETCH_HEAD
hint: Diverging branches can't be fast-forwarded, you need to either:
hint:
hint:   git merge --no-ff
hint:
hint: or:
hint:
hint:   git rebase
hint:
hint: Disable this message with "git config advice.diverging false"
fatal: Not possible to fast-forward, aborting.

[Josha Dekker]

I guess the solution should be straightforward, but I'm prudent because I don't want to make it worse (again)

[Eric Wieser]

git merge --no-ff is probably safe, git rebase is probably a bad idea

[Josha Dekker]

I did the --no-ff, then I get this:

         user name: joshadekker   host name: Joshas-MBP-2.home
        process ID: 65292
While opening file "/Users/joshadekker/Documents/Lean4/LeanMathlib/LeanMathlib/mathlib4/.git/MERGE_MSG"
             dated: Tue Jan 16 13:12:53 2024
      NEWER than swap file!

(1) Another program may be editing the same file.  If this is the case,
    be careful not to end up with two different instances of the same
    file when making changes.  Quit, or continue with caution.
(2) An edit session for this file crashed.
    If this is the case, use ":recover" or "vim -r /Users/joshadekker/Documents/Lean4/LeanMathlib/LeanMathlib/mathlib4/.git/MERGE_MSG"
    to recover the changes (see ":help recovery").
    If you did this already, delete the swap file "/Users/joshadekker/Documents/Lean4/LeanMathlib/LeanMathlib/mathlib4/.git/.MERGE_MSG.swp"
    to avoid this message.

Swap file "~/Documents/Lean4/LeanMathlib/LeanMathlib/mathlib4/.git/.MERGE_MSG.swp" already exists!
[O]pen Read-Only, (E)dit anyway, (R)ecover, (D)elete it, (Q)uit, (A)bort:

[Josha Dekker]

should I do E?

[Richard Copley]

This is from Vim and not from Git. Something went wrong with editing the commit message for the merge commit. Unless you put a lot of effort into the message, just delete it.

[Josha Dekker]

thanks, I think that worked!