search

coq-community / coq-nix-toolbox

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
MIT License
32 stars 9 forks source link

Disabling jobs only in CI. #62

Open Zimmi48 opened 2 years ago

Zimmi48 commented 2 years ago

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 commented 2 years ago

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).

CohenCyril commented 2 years ago

@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?

Zimmi48 commented 2 years ago

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

CohenCyril commented 2 years ago

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?

Zimmi48 commented 2 years ago

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

CohenCyril commented 2 years ago

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.