Zulip Chat Archive

Stream: new members

Topic: bors and pr_status


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

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

Johan Commelin (Jan 22 2022 at 20:57):

@Joachim Breitner Wow! This is great. Last time I checked, bors didn't seem to have this feature.

Bryan Gin-ge Chen (Jan 22 2022 at 21:02):

I think the setting has been there since before we started using bors, but I for one didn't understand the description in their docs until now.

Eric Rodriguez (Jun 25 2022 at 13:04):

awaiting-CI seems to have a bug:

image.png

The first commit is a PR too, so I think it's related

Bryan Gin-ge Chen (Jun 25 2022 at 13:35):

I'm out of time to investigate further, but here are some notes for my future self, or anyone who wants to take a look.

The issue is the following:

  • the first commit of #14947 is the same as the only commit of #14946
  • awaiting-CI was added to both
  • the build of #14946 finished (but not #14947)
  • awaiting-CI was removed from #14947 instead of #14946

Looking at the CI script, it looks like this is a known issue with the way we're getting the PR number.


Last updated: Dec 20 2023 at 11:08 UTC