Replace Bors with GitHub Merge Queue

Stream: mathlib4

[Tristan Figueroa-Reid]

Hi! Is there any reason why mathlib4 uses the (now being phased out) bors instead of GitHub's new merge queue?

[Andrew Yang]

Previous discussions on this might have some insights:
#general > bors going away?

[Eric Wieser]

I think the short answer is that the merge queue:

• has the wrong semantics, and runs CI in a way that doesn't work for us
• doesn't have the delegation behavior we use

[Tristan Figueroa-Reid]

I see - thanks!

[Kim Morrison]

I think there's also just a throughput issue! We have many days when we merge >20 PRs, and CI can potentially take an hour. Proper batching is required to make that feasible.