coq-nix-toolbox icon indicating copy to clipboard operation
coq-nix-toolbox copied to clipboard

Published 20 hours ago • verified publisher icon coq-community

Disabling jobs only in CI.

Open Zimmi48 opened this issue 4 years ago • 6 comments

In https://github.com/coq-community/paramcoq/pull/75, I had to put coqPackages.mathcomp.job = false; because I had also put coqPackages.mathcomp.override.version = "master"; but there was no reason to have a CI job building the full mathcomp.

In https://github.com/jwiegley/category-theory/pull/21, since no Cachix was set, I wanted to avoid the inefficiency of having dependencies built in separate jobs (only to be rebuilt in the main job). Therefore, I had to put a number of job = false; (more for the "dev" bundles than for the others). In the case of Coq, the unwanted consequence is that Coq is silently skipped when we try to build it, and it is only actually built later on, while trying to build ssreflect: https://github.com/Zimmi48/category-theory/runs/3493747463?check_suite_focus=true#step:10:9

There should be a way of excluding a job from CI without making nix-build --job a no-op.

Zimmi48 avatar Sep 02 '21 09:09 Zimmi48

Related to this, something that I still didn't understand is why some jobs marked as job = false; are still showing up in the GitHub Actions generated for this repo (e.g. coq-shell, and heq and mathcomp-bigenough in the master workflow).

Zimmi48 avatar Sep 17 '21 15:09 Zimmi48

@Zimmi48

I had to put coqPackages.mathcomp.job = false; because I had also put coqPackages.mathcomp.override.version = "master";

I do not understand this sentence. Why put job = false?

CohenCyril avatar Sep 22 '21 12:09 CohenCyril

Because otherwise the generated workflow contained a job building mathcomp (full) even though I only needed one for mathcomp-ssreflect IIRC.

Zimmi48 avatar Sep 22 '21 16:09 Zimmi48

Related to this, something that I still didn't understand is why some jobs marked as job = false; are still showing up in the GitHub Actions generated for this repo (e.g. coq-shell, and heq and mathcomp-bigenough in the master workflow).

This was a bug, I fixed it in #75, why exclude coq-shell, bigenough and heq though?

CohenCyril avatar Oct 29 '21 22:10 CohenCyril

Coq-shell, I don't know, but the rest of them are not really expected to be compatible with Coq master, are they?

Zimmi48 avatar Oct 30 '21 13:10 Zimmi48

Coq-shell, I don't know, but the rest of them are not really expected to be compatible with Coq master, are they?

I see I misread, I thought all of them were suppressed for released versions. I do not see why we would remove coq-shell I will keep it.

CohenCyril avatar Oct 30 '21 14:10 CohenCyril