CI launched even if not PR

[DmxLarchey]

Hi @yforster,

I am not sure if this is a bug but in the current configuration under my fork of coq-8.12, the CI is launched after every push, even if the current branch is not a pull request. I do not think it is needed to burn CPU cycles on devel branches which might be in alpha stage? Is this the behaviour you intended? Can you change this behaviour?

[DmxLarchey]

Ok I see, this in on line 3 of .github/workflows/build.yml ... there is both push and pull_request ...
Can we restrict the push to push on a branch which is actually a pull_request ?

[yforster]

I don't think disabling CI on push in genral is the way to go. We want the CI to check our main branches (if only just for the badges in the README to work), and I use CI for my development branches.

I see three ways to go:

• disable the CI on your branch by just deleting the build.yml file. It has to be added again when the PR is filed.
• we can add a no-ci keyword, which if occurring in a commit message disables CI
• we can configure CI to only check on push for branches starting with coq

Opinions? @fakusb @mrhaandi @dominik-kirst do you use the CI on your development branches? (I do!) Do you have preferences between the options?

[DmxLarchey]

Instead of no-ci keyword, maybe we could use the opposite ci keyword for commits on branches that are not PR which would then force the CI?

[mrhaandi]

Since the introduction of vos target I started to rely on CI for full compilation in my own branches on push instead of local compilation. Not to burn many CPU cycles on actual pushes I use local staging. Overall, my workflow already has minimal CPU cycle impact on (local + CI) CPU. If necessary, I can adapt to any of the three push suggestions. The most important point should be that a pull_request would not be affected in any way (no keywords etc.).

[yforster]

Instead of no-ci keyword, maybe we could use the opposite ci keyword for commits on branches that are not PR which would then force the CI?

That's not possible, we need the CI on arbitrary commits for the coq- branches.

We could add a rule that CI is not used if neither the branch is coq-* nor the keyword ci is present in the commit message.

[dominik-kirst]

I also use the CI on development branches, this is especially helpful when working with collaborators. I'm fine with the options mentioned, obviously no-ci would be more convenient than ci for me.

[yforster]

Alternative: We disable CI if the branch name contains no-ci or the following are both true: the branch name is not coq-* and the commit message contains no-ci.

[DmxLarchey]

That's not possible, we need the CI on arbitrary commits for the coq- branches.

I agree that CI for commits on the main branches of the main repo are mandatory! However, is it possible to distinguish forks from the main repo in the CI process?

Otherwise I am happy to comply with the most suited default behaviour of the CPU burners that surround me ;-) So the existence of the no-ci option would be fine with me.

But may be it could be documented? Indeed, I only noticed a CI was running on my fork because it failed I got an e-mail message. However, it was a partial commit that I expected to fail.

[DmxLarchey]

CI if the branch name contains no-ci

Not sure? Would it imply that CI will not run when the branch is converted PR ?

[yforster]

Logic is hard :) I'm trying again: We disable CI on push if either (1) the branch names contains no-cior (2) the branch name is notcoq-*and the commit message containsno-ci`.