Think about handling PR rollup merge race conditions

[Kobzol]

Just a thought I had today: if we have a PR A and a PR B, where B is a rollup containing A, we should make sure that once B is merged, bors won't start immediately merging A, in case the notification that A has been merged arrives too late and bors is very eager. It would be useful to check what homu does to prevent this (maybe it just sleeps for a minute after merging a PR, or something? :) ).

[jieyouxu]

I think the answer for homu(?) is it doesn't, rollup people have to be very careful not to include merged PRs or overlapping PRs.

[Kobzol]

Right, I guess that you could still do an "adversarial rollup", but normally homu won't try to merge a PR that was already merged in a rollup, even if it was in the queue before. I was thinking about the race condition where homu sees that PR A got to the top of the queue, but didn't realize yet that it was already merged as a part of another PR.

[Kobzol]

Bors should know about all rollups being created, since they are created through its website. Maybe we could report "pending" PRs in rollups in the DB, to avoid this. It would also help creating rollups, since bors would actually know in which rollups are other PRs included, and could give their checkboxes when creating a rollup.