CI launched even if not PR
Opened this issue · 10 comments
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?
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
?
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 withcoq
Opinions? @fakusb @mrhaandi @dominik-kirst do you use the CI on your development branches? (I do!) Do you have preferences between the options?
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?
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.).
Instead of
no-ci
keyword, maybe we could use the oppositeci
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.
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.
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
.
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.
CI if the branch name contains no-ci
Not sure? Would it imply that CI will not run when the branch is converted PR ?
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 not
coq-*and the commit message contains
no-ci`.