Do not run full CI by default, require full CI before merging.

[Zimmi48]

This was discussed during a Coq Call in late 2020: https://github.com/coq/coq/wiki/Coq-Call-2020-11-25

The idea was to distinguish between jobs that would be always run (lightweight mode) and jobs that would only be run on request (full mode). To ensure that we don't break the CI in master we should still require the full mode to be run on all PRs before merging. This could be ensured with a specific status check.

This has become less critical now and it's not clear that we still want this after:

• we got a Gold OSS plan on GitLab, lifting the 500 job limit;
• the auto-minimizer was added, which makes it much more valuable to get all the jobs to be run early (that being said, if we can get the test-suite to become complete enough to cover most failure cases, then this should become useful once more).

FWIW if / when we implement this feature, we could rely on the push option support of GitLab to specify if we are in lightweight mode or in full mode every time a PR is updated: https://docs.gitlab.com/ee/user/project/push_options.html#push-options-for-gitlab-cicd

[Zimmi48]

FWIW if / when we implement this feature, we could rely on the push option support of GitLab to specify if we are in lightweight mode or in full mode every time a PR is updated: https://docs.gitlab.com/ee/user/project/push_options.html#push-options-for-gitlab-cicd

This feature is now in use to manage the SKIP_DOCKER variable (fd01645).

[Zimmi48]

In today's call, we've determined that this feature was urgently needed and we've come up with the following interaction model.

• By default, coqbot runs a normal (light) CI.
• If a contributor wants a full CI, they need to put a label before pushing.
• coqbot takes this label into account (does a push to GitLab with FULL_CI=true) and removes the label immediately
• When reporting the pipeline to GitHub, coqbot indicates if this was a full CI or not based on the variables section in the pipeline webhook.
• When asked to merge a PR, coqbot checks if this was a full CI and if it is not the case, it triggers a full CI instead of merging. This was replaced by a use of a "needs" label to signal when the PR did not get a full CI.
• In addition, we could add a new command to ask coqbot to trigger a full CI without pushing.

[ejgallego]

It'd be nice if we manage to setup the light / heavy CI setup in such a way that the large job is a true superset of the lighter one.

That way, when caching is implemented better, the trigger of the heavier CI pipeline will reuse previous jobs.

Note that another way to implement this is make coqbot aware of incremental CI setup (so it triggers individual jobs instead of a full pipeline)

[Zimmi48]

Currently, FULL_CI=true adds jobs to the pipeline, but what could make sense would be to have another option REST_OF_CI=true or whatever that gives all the jobs that are part of the full CI and not the default one. In which case, when coqbot is asked to merge and the full CI was not run it runs only the remaining jobs. This assumes that the remaining jobs do not depend on any of the jobs from the default pipeline.

[SkySkimmer]

How do I get full CI to run for PRs where I'm the assignee not the author?

[Zimmi48]

There is no support implemented for this yet, so you still have to use the manual solution described in coq/coq#16600 (comment).

Now there is. See: coq/coq#16600 (comment)

[SkySkimmer]

I don't really like the label method. How about having a run full ci command instead?

[Zimmi48]

Done. See the updated coq/coq#16600 (comment).

FTR, I intend to wait before implementing the last step (@coqbot checks that a full CI was run before merging) because I wonder if implementing this is actually necessary and if we cannot trust the Coq maintainers to properly check whether it was the case (there are also legitimate reasons to not do it, e.g., if the PR was just missing a changelog and has not been force-pushed).

[Alizter]

What if coqbot added the "needs: full CI" label automatically to every PR. That way it would never merge unless the CI has run or the label removed.

[SkySkimmer]

With the current system it means the next push gets full ci

[Zimmi48]

But we could indeed consider something like this, for instance, coqbot adds a new label "needs: full CI before merging" to a PR when it runs a light pipeline on it (if the label is not already there) and it removes it when it runs a full pipeline (and puts it back at the next light pipeline). So, if the latest pipeline was not a full one, the assignee would have to manually remove the label to be able to perform the merge. That sounds like a reasonable enough solution that has the advantage of being more flexible than the one initially considered.

[Zimmi48]

And maybe it was a mistake to name the current label "needs: full CI" BTW. Maybe it should have been of a new category, like "request: full CI".

[Zimmi48]

FWIW, the solution proposed above was approved during the Coq Call yesterday and implemented today. The only remaining task now is to document the updated process.

[Zimmi48]

This is still missing from https://github.com/coq/coq/blob/master/CONTRIBUTING.md. Any help would be welcome.

[Zimmi48]

Fixed by coq/coq#17515.