search

coq-community / coq-nix-toolbox

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

coqPackages filters out incompatible packages by default. This is a problem when testing Coq dev. #25

Closed Zimmi48 closed 3 years ago

Zimmi48 commented 3 years ago

Almost no package in nixpkgs is marked as compatible with Coq, version "dev". The resulting behavior of the coq-nix-toolbox in the Coq repository is pretty confusing, e.g. nix-build --argstr job mathcomp-ssreflect will succeed immediately without building anything. Using ppRevDeps reveals that only two packages are not marked as incompatible with Coq, version "dev": heq and mathcomp-bigenough. But mathcomp-bigenough has incompatible dependencies, so running nix-build --argstr job mathcomp-bigenough leads to an error (but only after it has finished building Coq).

How to configure the nix-toolbox to avoid filtering out packages in coqPackages by default?

Zimmi48 commented 3 years ago

Actually, nix-build --argstr job mathcomp-bigenough fails immediately with:

nix-build  --argstr job mathcomp-bigenough
error: Package ‘coqdev-mathcomp-ssreflect-broken’ in /nix/store/a4sl40d2mj202a4xc90clbhvhp08vai0-source/pkgs/build-support/coq/default.nix:67 is marked as broken, refusing to evaluate.

When inside nix-shell, it behaves differently (succeeds by building /nix/store/19vaa104a75ydi8kigyvficpjqnkvqaf-coq-dev only) which might be a bug.

Zimmi48 commented 3 years ago

OK, so one possible answer is pretty similar to #24: just expand the default bundles to override the version of reverse dependencies and use their master version.