feat(bors.toml): let bors wait for PRs to be green before merging

[nomeata]

This makes it reasonable to type bors r+ even while CI is running.

---

See discussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/bors.20and.20pr_status/near/268977363

[bryangingechen]

Let's see if this works the way I think it does...
bors r+

[bors]

🕐 Waiting for PR status (Github check) to be set, probably by CI. Bors will automatically try to run when all required PR statuses are set.

[nomeata]

Interesting, this means that bors uses the configuration in the PR, not the one in master. Good to know.

[bryangingechen]

Yep, that feature's been very useful for testing!

[bryangingechen]

Ah, since bors uses the bors.toml in the PR, I guess that means that even after this is merged, we still can't safely use bors r+ on older PRs (unless they've had master merged into them).

[bryangingechen]

Looks to me like the required checks passed, but this doesn't seem to be in the bors queue yet. Does it usually take a while?

[nomeata]

I’m not sure. Maybe we have to wait for the next merge batch?

[nomeata]

Looks to me like the required checks passed, but this doesn't seem to be in the bors queue yet. Does it usually take a while?

Oh, I remember a problem we had with bors at my previous job: At some point in the past it would timeout in that “waiting state” without notice.

Not 100% related, but if this issue were fixed we’d have more clarity: bors-ng/bors-ng#1140

Are we running our own instance of bors, or is this a hosted github action? Maybe something needs to be configured to allow bors to actually react on a status change?

I can open an issue at the bors repo to ask, but not today…

[nomeata]

bors ping

[bors]

pong

[nomeata]

Or maybe bors gets confused because the configuration on master is different? (Just guessing)

[bryangingechen]

We're using the publicly hosted instance of bors at the moment. Let me try again and see what bors has to say:
bors r+

[bryangingechen]

Ah, that makes sense. If the checks are already green, it goes on the queue automatically. Let me take this off for now.
bors r-

[bors]

Canceled.

[bryangingechen]

If bors is likely to silently timeout while waiting for checks to pass then it's not clear that this will be an improvement. I'd like to have a better understanding of what happened here (and get some more opinions from the other maintainers) before merging this. Joachim, if you don't mind creating an issue that'd be greatly appreciated!

[nomeata]

@bryangingechen, based on reading the bors code, this might fix the problem for us. It’s still suboptimal user experience that if that (huge) timeout is exceeded, that there is no message, but maybe that’s rare enough. _{If you want a good UI with better insight, we should switch back to mergify ;-)/}

[bryangingechen]

Thanks! Let's go with this for now! I've just rerun the CI jobs on the last commit, so let's see how this goes:
bors r+

[bors]

🕐 Waiting for PR status (Github check) to be set, probably by CI. Bors will automatically try to run when all required PR statuses are set.

[nomeata]

Nope, still doesn't work, it seem :-(

[nomeata]

Do we actually need an approving review maybe?

[collares]

It might still work! Bors polls GitHub every 5 minutes according to https://github.com/bors-ng/bors-ng/blob/a1b31786d48839f67fd5691564217e8538f74b24/lib/worker/batcher/bors_toml.ex#L20

Edit: Nope :( And besides, Bors now GitHub polls every minute, the comment just wasn't kept up to date.

[bryangingechen]

I'm going to try again with the approving review, but even if it works this time, I think I'll take it off the queue again until we can figure out exactly what the conditions are...
bors r+

[bors]

🕐 Waiting for PR status (Github check) to be set, probably by CI. Bors will automatically try to run when all required PR statuses are set.

[nomeata]

:-(

[ericrbg]

agh, this is very sad :( I was excited for this

[nomeata]

I was hoping that upstream can help us out here, but the issues there have been silent so far.

[bryangingechen]

The maintainer has kindly helped us out with various issues before; they may just be busy at the moment.

[collares]

Do mathlib maintainers have access to bors logs?

Also, after the tests passed, did anyone check https://app.bors.tech/repositories/24316 to see if this PR was still awaiting review? I guess so, but the reason I ask is because bors sends a comment in every failure case (even timeouts), but it stays silent when it detects PR checks succeeded (the rationale being that the staging commit will reference the PR, which is enough of a notification). If there's an already-running batch, this means nothing will show up here for a few hours.

[bryangingechen]

@collares We have access to the log page, but as far as I can tell, this PR doesn't appear there (either as a failure or success). Also, I did look at the main page several times and again, I never saw this PR move off "Awaiting Review" status. I haven't looked at the bors code yet, but I would have expected that after the checks pass, this PR should be moved to "Waiting to Run" and then a staging commit should get pushed once all other batches are finished, but that never happened.

[collares]

Ah, that's sad :( So the log doesn't even contain the "Continue Poll Patch #{patch.id} prerun" messages? They are logged once per minute, each time bors polls the check status. I assume every such log message refers to this PR, even if the patch ID is something unrecognizable (could be just a unique ID unrelated to the PR number/commit sha).

[nomeata]

JFTR, I don't have access to https://app.bors.tech/repositories/24316/log, so i can't help with the sleuthing

[bryangingechen]

So the log doesn't even contain the "Continue Poll Patch #{patch.id} prerun" messages?

For the record, this is what the log page looks like (I'm only showing the top of the page, but you can keep clicking "Older" at the bottom of the page to load more and more batches):

Every once in a while, bors crashes and we get something which looks like this:

PR number 11609 doesn't show up anywhere on that log page, so unfortunately I don't think there's much we can learn from it.

If we want to continue chasing this down on our side, someone could try setting up a private bors instance and trying to reproduce this issue there. I know that @gebner set one up in the past for testing - if it still exists, maybe he can give access?

[gebner]

if it still exists, maybe he can give access?

Yes, https://borslein.herokuapp.com/ is deployed from https://github.com/gebner/bors-ng

If you want I can give you push access. But it's also super easily to deploy your own instance.

[collares]

Thanks @gebner! It's indeed very easy to deploy it to Heroku; I had to override the Node version to avoid a build error but otherwise it went smoothly.

I reported my findings in the issue filed by @nomeata (bors-ng/bors-ng#1434), but the TL;DR is that bors just randomly stops polling for changes, and typing r+ again wakes it up for a while. If it is awake when the CI checks pass, it creates a batch normally (even if the r+ happened prior to the completion of the CI run, of course). The logs aren't really useful and I don't have any Erlang runtime debugging skills.

EDIT: Turns out bors stops the batch-polling process if it doesn't find any "incomplete" (i.e., waiting to run) batches after a poll, which was a valid optimization before the same process handled polling pr_status checks as well.

[bryangingechen]

@collares thanks very much for following up on this! Let's hope this moves things forwards!