GitHub merge-conflict label

Stream: general

[Martin Dvořák]

When I get a merge-conflict label on a Mathlib PR, can I view on GitHub where the conflict is?

[Johan Commelin]

Usually there is a button "Resolve conflicts" close to where the merge button normally is.

[Martin Dvořák]

Ah! It's just a conflict in the Mathlib.lean file. IMO it's pretty dumb we have to maintain this file.

[Johan Commelin]

Yep. At least we should have a bot that fixes these conflicts.

[Martin Dvořák]

The current merge-conflict mechanisms imply that other PRs can kick my PR out / to the end of #queue .

[Jireh Loreaux]

I think several maintainers look at the queue in both ascending and descending order. I do anyway.

[Riccardo Brasca]

#12780 got a merge conflict, and the bot corrected added the merge-conflict label. On the other hand, it didn't remove it once the conflict was resolved. Does anyone know why? The same happened with #13287

[Riccardo Brasca]

I did remove the label, sorry for the noise.

[Anne Baanen]

Apparently it was just very slow!