Is there a way to make this do the stronger thing of not running until ci actually passes?

Not as far as I know. Either way, I think there's benefit to merging this PR as is; it means that it's not possible to merge something without CI unless you consciously remove a label. @kbuzzard did so accidentally earlier today.

But if people never add the label in the first place we still have an issue is my point. Perhaps we need an action to automatically add the label if bors cannot be conditional on ci passing itself.

Looking at the bors reference https://bors.tech/documentation/ the pr_status config option sounds like it might do the right thing. I'm on a plane so I can't check the bors source right now to confirm but if that option does allow us to actually wait for status checks rather than a label (which can be misapplied) that sounds a far better but equally simple fix than what you propose here

https://github.com/bors-ng/bors-ng/blob/390d99890d16a9fa34691728812d0052e99131f4/lib/worker/batcher.ex#L972

Looks like it does do the right thing, waiting on any statuses mentioned there to be not in process or unset, and erroring if they fail.

Sometimes we want to override that deliberately though, which I assume that does not let us do? I still think the approach we had in mathlib 3 and that this PR enables, while not perfect, is better than what we have now.

I don't know why we would want to override it? Just to get something into master <=1hr faster? I assume priorities would still be helpful in such a situation, or at worst pushing directly to master if something that the maintainers truly wanted in master instantly came up?
We can put it to a vote on zulip perhaps, I'd say enforcing this rule is an improvement over the old behaviour, as tags are basically just human curated at the end of the day.

I don't know why we would want to override it? Just to get something into master <=1hr faster?

Yes: for instance if a PR is green but someone requests a typo fix in documentation, there's little point in waiting for a CI run. It would of course be better if the CI run could also be cancelled to save resources.

pr_status has been discussed before on Zulip, but didn't work in leanprover-community/mathlib3#11609.

I worked out why this option is missing from mathlib4; it was added in mathlib3 a day or two after the mathlib4 repo was set up, so I've labelled this with mathlib-pair as this is a forward-port!

bors merge

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style