I am trying to test a package that depends on MathComp using Coq 8.17 and the Nix toolbox. I ran the commands to set up the initial configuration files. Then, I defined a bundle with the following line:
coqPackages.coq.override.version = "8.17+rc1";
When I run
nix-shell, I get the following output:
error: Package ‘coq8.17-mathcomp-ssreflect-broken’ in /nix/store/a0m398jx1lmxj0q7b79l4khvwsxm8634-source/pkgs/build-support/coq/default.nix:84 is marked as broken, refusing to evaluate.
I had run
nix-shell a few times before trying to add some lines for mathcomp and ssreflect, which is why it might be complaining about them now. In any case, the current bundle only tries to override Coq itself.
If I try to enable broken packages, I get the following error:
$ NIXPKGS_ALLOW_BROKEN=1 nix-shell these 2 derivations will be built: /nix/store/4kk5r9ff2w0j98qwzl1czwsfins824ig-jsonAction.drv /nix/store/s3lwabj8nsq2gzcljrzvfq3wfwz978vb-coq8.17-mathcomp-ssreflect-broken.drv building '/nix/store/4kk5r9ff2w0j98qwzl1czwsfins824ig-jsonAction.drv'... building '/nix/store/s3lwabj8nsq2gzcljrzvfq3wfwz978vb-coq8.17-mathcomp-ssreflect-broken.drv'... unpacking sources variable $src or $srcs should point to the source error: builder for '/nix/store/s3lwabj8nsq2gzcljrzvfq3wfwz978vb-coq8.17-mathcomp-ssreflect-broken.drv' failed with exit code 1
Any idea how I might fix this?
MathComp is not yet available for coq 8.17 in NIx, c.f.: https://github.com/NixOS/nixpkgs/pull/220000
@Arthur Azevedo de Amorim Thanks to @Pierre Roux it's now available if you update the toolbox
nix-shell https://coq.inria.fr/nix/toolbox --arg do-nothing true --run updateNixToolBox
Arthur Azevedo de Amorim has marked this topic as resolved.
Last updated: Dec 07 2023 at 14:02 UTC