Stream: Nix toolbox devs & users

Topic: ✔ Running Coq 8.17

view this post on Zulip 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:

these 2 derivations will be built:
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?

view this post on Zulip Pierre Roux (Mar 08 2023 at 21:45):

MathComp is not yet available for coq 8.17 in NIx, c.f.:

view this post on Zulip 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 --arg do-nothing true --run updateNixToolBox

view this post on Zulip Arthur Azevedo de Amorim (Mar 09 2023 at 16:23):

Great; thanks!

view this post on Zulip Notification Bot (Mar 09 2023 at 16:23):

Arthur Azevedo de Amorim has marked this topic as resolved.

Last updated: Dec 07 2023 at 14:02 UTC