Switch to GH merge queue?

[RalfJung]

The idea of switching from bors to GH merge queues has come up multiple times. "Old" bors often has trouble (though in the recent past it worked just fine), and IIRC, t-infra recommends that most smaller projects switch to merge queues rather than "new" bors. This also has the advantage of working around rust-lang/rust#101907 since we'd no longer have bors commits as part of the sync.

The main downside is increased latency: github waits until PR CI passes before even putting the PR in the queue, so one can't just push + r+ immediately, one has to wait for two times the CI time until the PR actually lands. However, landing PRs is rarely latency-sensitive so I don't think this is a big enough problem.

@rust-lang/miri what do you think?

[oli-obk]

Can we set PR CI to make all CI runs "optional", so their failure is irrelevant. That may allow the merge queue addition, we just need to ensure that the merge queue actually requires the CI runs to pass

But yea, seems fine to me

[RalfJung]

Can we set PR CI to make all CI runs "optional", so their failure is irrelevant. That may allow the merge queue addition, we just need to ensure that the merge queue actually requires the CI runs to pass

That would probably lead to confusing UI where there are green checkmarks even though CI failed...

[oli-obk]

No, you can set CI runs as not blocking the merge button from becoming green. Even if the CI run shows up red. The only question is if we can make the merge queue have different CI rules than the PR CI

[RalfJung]

Oh, you mean changing what is set in "Require status checks to pass before merging"... I think that's always the same. But we could make the success job actually be different depending on whether it is a PR CI run or a merge queue CI run, and make it succeed immediately in PR CI, maybe that would make it enqueue things immediately.

But it's not worth it IMO. Our CI times are <30min, so landing takes <1h, which seems entirely fine.

[RalfJung]

@saethlin what do you think?

[saethlin]

The runtime seems acceptable. I've been getting a lot of practice working with merge queues at my day job, so I'm more confident switching than I was the first time you mentioned this topic.