Summary: Keep track of when a pull request is unmergeable, or a draft, and reject them.
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.
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.
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.
It adds two new columns to the database, and one new column to the dashboard.
- 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.
- It's the design that homu uses.
I'm not really aware of any.
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.
- Implemented by https://github.com/bors-ng/bors-ng/pull/1159