have Mergify insist on all-green CI

[geekosaur]

GitHub's branch protection rules just don't cut it. (As a result, neither does GitHub's merge queue.)

Template B: This PR does not modify behaviour or interface

E.g. the PR only touches documentation or tests, does refactorings, etc.

Include the following checklist in your PR:

• Patches conform to the coding conventions.
• Is this a PR that fixes CI? If so, it will need to be backported to older cabal release branches (ask maintainers for directions). (It does, but Mergify only reads the configuration on master.)

Closes: #10365

[geekosaur]

At some point we'll also want to decide whether to remove the current checks from the branch protection rules, which will also require restricting who has access to GitHub's merge button.

[ulysses4ever]

I think the commit message and PR description should explain more of your findings and how they shaped this change.

[geekosaur]

It's still a draft for a reason; I'm still double-checking things.

[geekosaur]

Summary: GitHub's branch protection rules require you to list all jobs which must succeed, or use something like our "post job" hacks which fold an entire workflow's jobs into a single checkable job (but this only works within a single workflow, so you would need one for every workflow definition and need to list all of those). This seems remarkably error-prone, not to say bass-ackwards. (Is there ever normally a case where you don't want all-green CI? Note that exceptional cases can be dealt with using the merge button, which doesn't involve Mergify but does as currently configured require an administrator.) Since GitHub's own merge queues are driven by branch protection rules, they have the same ridiculous requirement.

Mergify, on the other hand, provides a convenient way to require green CI: the #check-failure=0 condition. No need to list out all the possible jobs, or worry about missing one. Any failing jobs will prevent merging. (Failure here includes timeouts and canceled jobs; conversely, skipped jobs are considered to be successes. In short, it's sensibly defined.)

I have also taken the liberty of requiring merge+no rebase PRs to be up to date (meaning, rebased by the author or other user with access to the organization) before they can be merged. It seems to me that you'd want this requirement to avoid problems, since you don't have a merge queue to ensure compatibility, and Mergify can't do the rebase itself or we wouldn't be using that label.

[geekosaur]

I should also mention that many of the exceptions that might require manual merges can also be dealt with by cherry-picking fix commits from other PRs; this is how I got the 3.12 branch working again. This doesn't cause conflicts, since git will recognize the commit(s) as already being applied.

[geekosaur]

What I don't know yet is if this will fix the premature merge issue. I suspect that one's harder, though, especially since it's proving difficult to pin down. I will need to catch several of them in the act and examine their checks to see what commonality they have. Relationship to the skip jobs is only a slightly educated guess backed by the few I've seen involving the skip job, but the black swan rule applies.

[geekosaur]

This is ready; I'm just periodically rebasing.

[geekosaur]

I propose we skip the delay, so we can avoid a repeat of the temp file changes colliding and CI not catching it because they were merged before CI finished. (I will still monitor commits after this goes in to verify that it works.)

[ulysses4ever]

Agreed

[Mikolaj]

Thank you.

[ulysses4ever]

I think the commit message and PR description should explain more

It's still a draft for a reason

Well, now it's merged but the message wasn't updated. That's why I think it's always a good idea to put as much as you know as soon as possible and thinking "I'll do extensive research first" is a slippery slope.