Zulip Chat Archive

Stream: general

Topic: Merge conflicts

Damiano Testa (Apr 06 2021 at 10:25):

Dear All,

a batch of PRs are trying to get merged, but CI failed to incorporate them in mathlib. I am the author of one of them (PR #6993), I see that bors says that there are merge conflicts, but does not actually say what the conflicts are (or, at least, I cannot figure it out).

Is there something that I can/should do? Will it simply fix itself by running yet another time?

Thanks!

Eric Wieser (Apr 06 2021 at 10:27):

It means that your PR conflicted with another one in the batch

Eric Wieser (Apr 06 2021 at 10:27):

If that batch succeeds, then github will show you what the conflict is once the thing it conflicts with is in master

Damiano Testa (Apr 06 2021 at 10:28):

Ok, but it already failed a couple of times and I do not know where to look for the merge conflict...

Eric Wieser (Apr 06 2021 at 10:28):

I only see the one failure

Eric Wieser (Apr 06 2021 at 10:29):

Your PR is still in the queue: https://app.bors.tech/repositories/24316

Damiano Testa (Apr 06 2021 at 10:30):

Yes, but this one, another PR from the same batch as mine, also has a similar status:
https://github.com/leanprover-community/mathlib/pull/7055

I imagine that (some of) the others would, as well.

Damiano Testa (Apr 06 2021 at 10:30):

The PR went back into the queue already. After after having been "yellow" for a while, it got the red cross and went back into the queue.

Damiano Testa (Apr 06 2021 at 10:31):

This happened a few times today.

Damiano Testa (Apr 06 2021 at 10:32):

It seems a good explanation that there is some merge conflict internal to the batch that is preventing bors to merge, but I do not know how to figure out what the conflict is.

Anne Baanen (Apr 06 2021 at 10:33):

Bors is now bisecting the commits, trying to figure out which batch of commits causes the failure

Damiano Testa (Apr 06 2021 at 10:33):

Ah, ok! So the approach is to sit and wait and, at some point, there will be a conflict to repair, right?

Thanks for the explanation!

Anne Baanen (Apr 06 2021 at 10:37):

If the currently running batch succeeds, they will just be merged. If it fails, bors will try again with half of the commits, until it finds the PR(s) causing the failure.