Arthur Azevedo de Amorim (Mar 08 2023 at 21:28): Arthur Azevedo de Amorim (Mar 08 2023 at 21:28):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?
Pierre Roux (Mar 08 2023 at 21:45):MathComp is not yet available for coq 8.17 in NIx, c.f.: https://github.com/NixOS/nixpkgs/pull/220000
Cyril Cohen (Mar 09 2023 at 13:33):@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
Great; thanks!
Notification Bot (Mar 09 2023 at 16:23):Arthur Azevedo de Amorim has marked this topic as resolved.
Last updated: Sep 15 2024 at 12:01 UTC