Zulip Chat Archive

Stream: general

Topic: Merge conflicts


view this post on Zulip 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!

view this post on Zulip Eric Wieser (Apr 06 2021 at 10:27):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Eric Wieser (Apr 06 2021 at 10:28):

I only see the one failure

view this post on Zulip Eric Wieser (Apr 06 2021 at 10:29):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Apr 06 2021 at 10:31):

This happened a few times today.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Anne Baanen (Apr 06 2021 at 10:38):

(I don't see an obvious conflict from the PR descriptions at least.)

view this post on Zulip Floris van Doorn (Apr 06 2021 at 15:32):

#7021 had a merge conflict, which I fixed.

view this post on Zulip Eric Wieser (Apr 06 2021 at 15:35):

Thanks!


Last updated: May 12 2021 at 04:19 UTC