bors merge conflict

Stream: new members

[Joachim Breitner]

Bors says “merge conflict” for some of my PRs, but if I locally pull master into my branch, I don’t see a merge conflict, so I am not 100% sure what it means.
Do I have to do something or is this a transient problem?
(#12589, #12473, #12524)

[Johan Commelin]

It's probably a different PR in the same bors batch.

[Joachim Breitner]

Ok, so I'll just wait for that batch to land in master and then resolve any conflicts.

[Joachim Breitner]

Is it expected that the Details link of the bors status is not visible to mere mortals? At https://app.bors.tech/repositories/24316/log I get “Permission denied”

[Bryan Gin-ge Chen]

Unfortunately that seems to be the case. That link just shows a list of past batches and their statuses though. Screen-Shot-2022-03-11-at-11.51.41-AM.png

[Mauricio Collares]

Joachim Breitner said:

Is it expected that the Details link of the bors status is not visible to mere mortals? At https://app.bors.tech/repositories/24316/log I get “Permission denied”

The bors "merge conflict" failure reveals the batch number if you look at the "Details" URL (https://app.bors.tech/repositories/24316/log#batch-202278 in your case). You can then go to https://app.bors.tech/batches/202278 to see what other PRs were included in the batch.

[Mauricio Collares]

But it might be the case that two of your PRs conflict (by git standards), since #12473 and #12589 both touch prod_le_of_forall_le or a nearby function.

[Joachim Breitner]

Right, but I would expect that one of them goes through then.

[Mauricio Collares]

That will probably happen but the fact that it's pending doesn't get reflected on the GitHub status thingy because the smaller batches are still waiting to run. It will probably turn yellow again once the corresponding batch starts.

[Bryan Gin-ge Chen]

The fact that there's a red x instead of a yellow dot when there's a merge conflict is the subject of this issue: https://github.com/bors-ng/bors-ng/issues/1227

[Mauricio Collares]

@Joachim Breitner I guess you know this already, but the pending batches can be viewed at #bors (it's publicly accessible but requires GitHub auth)

[Joachim Breitner]

Thanks , I did not!

[Kyle Miller]

The Lean version bump #12591 was part of this batch --it seems to merge cleanly into master, but I haven't recompiled everything to check. Is it safe to try a bors merge again?

[Bryan Gin-ge Chen]

@Kyle Miller Which PR did you want to try bors merge on? #12591 and the 3 PRs in Joachim's first comment are all still on the queue at #bors as far as I can tell.

[Kyle Miller]

Oh, missed that, thanks.