Right now, bors checks whether a pull request is "not mergeable" according to GitHub's API, before it tries to merge it. This is good, but it's kinda late at that point. The pull request webhook actually reports whether it's mergeable in advance, so if bors used that, it would be able to reject it earlier and avoid wasting time, and it could show that information on the pull request dashboard.
Guide-level explanation
This change is almost completely transparent to the user, and would basically only change the behavior in very weird corner cases, like if they queued a pull request that wouldn't merge cleanly into the main branch behind another one that actually fixed the merge conflict.
Reference-level explanation
Bors will check whether your pull request is mergeable both before enqueueing it, and after dequeueing it.
Bors will also refuse to merge draft pull requests.
Drawbacks
It adds two new columns to the database, and one new column to the dashboard.
Rationale and alternatives
By adding it to the database, bors can also show it in the dashboard, which makes it a bit more useful (whether a pull request is mergeable or not seems important).
The current one uses slightly less code, but it's probably not what we want.
Right now, we don't pluck unmergeable pull requests out of batches, but probably could change to do that. I don't think it would actually make much difference, performance-wise, but it would make the dashboard a bit more accurate.
One thing that I did in our private repo is canceling a merge conflict and kick that PR out of the queue. For example, I have PR#1 and PR#2.
Both PR can be merged directly to the main as they have no conflict with the main branch. But they conflict with each other. IIRC the existing implementation when that happens is splitting the batch into two smaller batches. For context, we are using squash mode, where each PR becomes a single commit.
What we did is when creating the staging branch, and the process crashed, we canceled the latest commit and comment on that PR that their PR conflict with one of the commits in the batch.
The new batch will have all existing PR, but the one that gets canceled.
When we have more than 5 commits, it'll be faster than having it splits multiple times because of the conflict.
What’s actually in bors nowadays is a bit more sophisticated than that, but it’s not quite what you’re doing. It’s written here, and what it does is isolate batches that can’t be merged into the main branch (so we can avoid repeatedly splitting a batch when it’s obviously just one PR causing the trouble), but if GitHub says all the branches are mergeable, then it’ll split in half as normal.
What you’re describing sounds a bit “winner takes all,” which is why I don’t like it. One thing we might do, that isn’t quite as extreme as outright cancelling whichever one happens to come last, but should still be faster than splitting in half, is implicitly set the single flag on it. That way, if the batch winds up failing, the single PR that “lost” will still be in the queue to try to get in.
Yes, most of the conflicts (if not all) that happened in our case is when GitHub says all the branches are mergeable. Using single is an interesting alternative. One concern with that alternative is, the PR won't be able to get in anyway. Rather than spending time on the queue that slows down processing another batch. In theory, it should only be adding up 1 minute, but in a fast-paced period where we are merging tens of PR at a time, it added up.
In any case, the improvements you're talking about don't actually conflict with any of these changes. So to avoid blocking this forever, it's entering FCP. Disposition: accept.
