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:

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

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.: https://github.com/NixOS/nixpkgs/pull/220000

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 https://coq.inria.fr/nix/toolbox --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: Mar 28 2024 at 09:01 UTC