Zulip Chat Archive

In previous projects that used bors (or mergify) I was used to be able to tell bors to merge, and it would wait for the PR CI to turn green. It seems that this is not the case here, and contributors are expected to manually wait and check for CI to turn green before entering bors r+, which seems like an odd use of our attention…
Bors does support waiting for a PR to turn green, using the pr_status configuration option, so I wonder if this is intentionally not used here (and why? maybe to merge fast when it’s a trivial change?), or whether it’s maybe simply a newer feature that wasn’t considered yet?

Joachim Breitner (Jan 22 2022 at 20:38):

(I found https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/bors.md which explains why bors was chosen, but it doesn’t answer this question. And as a NB, mergify has improved a lot since then, including the ability for merge trains with speculative tests, taking commit messages from PR descriptions, tracking PR dependencies – not suggesting to switch back, but pointing out that it may have become a viable option again, in case bors falls out of favor)

Bryan Gin-ge Chen (Jan 22 2022 at 20:42):

Oh, I didn't realize that option meant that we could configure bors to wait for certain checks to pass on the final commit! If you're familiar with this setting, do you mind submitting a PR to help us make use of it?

Joachim Breitner (Jan 22 2022 at 20:43):

Not familiar, but it seems straight forward enough. Will prepare a PR.

Joachim Breitner (Jan 22 2022 at 20:44):

(Hmm, it may be that with mergify you even get “properly merged PRs” despite using squash merge + merge trains… that might actually be worth evaluating at some point if this “Closed by bors” business becomes too annoying.)

Joachim Breitner (Jan 22 2022 at 20:46):

https://github.com/leanprover-community/mathlib/pull/11609. But probably Bryan should double-check that this is what you want :-)

Joachim Breitner (Jan 22 2022 at 20:47):

Wait, I am talking to Bryan. I should pay attention to Zulip the same way I do to git log :-D

Bryan Gin-ge Chen (Jan 22 2022 at 20:53):

Wow, bors even posts a message telling us that it's waiting for the checks to pass! This is great!

As a follow up we might want to see if we want to change the way the "awaiting-CI" label works (as right now, the label blocks bors r+ and is removed automatically at the end of CI), but I think this is good for now.

cc: @Johan Commelin