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.
Anne Baanen (Apr 06 2021 at 10:38):
(I don't see an obvious conflict from the PR descriptions at least.)
Floris van Doorn (Apr 06 2021 at 15:32):
#7021 had a merge conflict, which I fixed.
Eric Wieser (Apr 06 2021 at 15:35):
Thanks!
Yaël Dillies (May 02 2022 at 23:16):
@Scott Morrison, are you really managing the tags of #13798 live or is there some Github witchcraft going on?
Scott Morrison (May 02 2022 at 23:16):
Ah!
Scott Morrison (May 02 2022 at 23:17):
Because of the API rate limits, we decided to "diversify" the API tokens we're using to run various bots.
Scott Morrison (May 02 2022 at 23:17):
For now the merge conflict bot is running off a token from my account, so it says it is me. :-)
Scott Morrison (May 02 2022 at 23:17):
I will go create a new account and replace the token soon!
Scott Morrison (May 02 2022 at 23:17):
(This doesn't require a new PR.)
Yaël Dillies (May 02 2022 at 23:18):
Ah! And people are still saying that an AI can't do theorem proving?
Last updated: Dec 20 2023 at 11:08 UTC