Require status checks to pass before merging (for auto-merge, no policy change)

[andres-erbsen]

I would like to use the "Enable auto-merge" feature of GitHub, to mark PRs to be merged as soon as CI passes. I have used it extensively in my own repositories and found it to be reliable, and a good way to reduce friction for contributing. However, this feature is limited to branches with a branch-protection rule preventing merging without a passed check:

The option to enable auto-merge is shown only on pull requests that cannot be merged immediately. For example, when a branch protection rule enforces "Require pull request reviews before merging" or "Require status checks to pass before merging" and these conditions are not yet met. For more information, see Managing a branch protection rule.

Further, branch protection rules must explicitly enumerate checks that pass, which seems impractical given the current fine-grained check granularity. If that granularity is to stay, I believe the actual configuration would have to be as follows:

1. Add a job that fails unless all other jobs succeed (depending on the other jobs is not good enough because dependency failures cause "skipped", not "failed"). There's a marketplace action called "alls-green" that may be useful for inspiration.
2. Configure a branch protection rule for master to require CI checks to pass before merging. This way not-yet-passing PRs can be set to merge once CI passes.
3. Enable the "bypass branch protections" for all roles with the merge permission. This way, non-passing PRs can still be merged.

I would be happy to try hand at configuring this myself if I had the requisite permissions. If this is not desired, I'd be happy to help out.

[Zimmi48]

I agree with this plan.

Just to clarify things for people, like me, who have never used the feature, it's not going to auto-merge PRs that have not been reviewed, just because CI passed. It's a feature similar to the long requested @coqbot: merge when CI passes feature request (rocq-prover/bot#108), i.e., it needs some action from a maintainer with merge permissions.

Besides, I think it's good to start activating branch protection rules, independently of the auto-merge feature.

I'm fine with using the alls-green action. The main issue that I see with this plan is that you still need to manually list all the other jobs in the all-greens dependencies, and this has to be done in a workflow file which is otherwise auto-generated. Perhaps, a more pleasant strategy would be to add this all-greens job (or equivalent) directly into the Nix Toolbox code for generating these workflows: https://github.com/rocq-community/coq-nix-toolbox/blob/52aaa743836510268bf94deb898de0f8bd0501be/action.nix#L150

@andres-erbsen I've given you admin permissions to the repository. In the future, I would like to have a dedicated stdlib-admins team, instead of managing these permissions by user.

[andres-erbsen]

Indeed, I had missed that alls-green also requires maintaining an exhaustive list. I am now confused why it exists at all...

The Nix-toolbox-based approach seems promising, but I think I would have a hard time figuring out how to implement that. Looking around some more, I found https://github.com/apps/mergery . Though it looks somewhat rigid and opaque, and I can't find the source anywhere...

[proux01]

Action files are generated from the action.nix file. I guess you can add your "all-greens" job to the list on line
https://github.com/rocq-community/coq-nix-toolbox/blob/master/action.nix#L150 taking example on what's done a few lines before. In particular, you want to add all jobs in the needs field I guess
https://github.com/rocq-community/coq-nix-toolbox/blob/61a1c4da3df5ff208a9d735e64e4039c5066b31c/action.nix#L124
I agree that the syntax of the nix language is... strange to say the least (x: b means fun x => b) but it's essentially a (unfortunately) dynamically typed functionnal language.