yeah that dune error is because make cannot find the dune exec. You need to do what Cyril says and activate dune in the derivation so that nix makes it available for make.
Pierre Roux said:
I guess
mathcomp = "2.0"
should bemathcomp = "2.0.0"
and maybecoq = "8.17"
should becoq = "8.17.0"
FWIW, using just "8.17" is fine when nixpkgs knows about an 8.17 version (it will choose the last one). The problem here was that Pierre was using an old nixpkgs version which didn't contain Coq 8.17, and Coq derivations have a fallback for versions they do not know about.
Pierre Jouvelot said:
Pierre Jouvelot said:
Ali Caglayan said:
Is your nixpkgs too old to have 8.17?
Ali Caglayan How do I update those?
For the record, I found the following command to update the nixpkgs:
nix-channel --update; nix-env --install --attr nixpkgs.nix nixpkgs.cacert
but that doesn't fix the problem, and the same error message occurs.
nix-channel --update
indeed doesn't help because the toolbox is using a pinned nixpkgs. You can either update the toolbox itself, or the nixpkgs revision it uses. Cf. updateNixToolBox
and updateNixpkgsUnstable
functions provided by the Coq Nix Toolbox nix-shell
.
Oops, I hadn't seen that Cyril had already replied with the same information.
Ali Caglayan said:
yeah that dune error is because make cannot find the dune exec. You need to do what Cyril says and activate dune in the derivation so that nix makes it available for make.
Indeed. All worked fine after a nix-env -i dune
. Thanks a lot @Ali Caglayan @Cyril Cohen @Pierre Roux @Théo Zimmermann
Pierre Jouvelot has marked this topic as resolved.
Pierre Jouvelot said:
Ali Caglayan said:
yeah that dune error is because make cannot find the dune exec. You need to do what Cyril says and activate dune in the derivation so that nix makes it available for make.
Indeed. All worked fine after a
nix-env -i dune
. Thanks a lot Ali Caglayan Cyril Cohen Pierre Roux Théo Zimmermann
It's a bit dangerous to mix pure and impure derivations... if it works for you right now I guess it's ok, but it may break unexpectedly in the future and it will definitely not work if you release your development.
If you are having trouble finding dune in nixpkgs, it is named dune_3
Last updated: Oct 13 2024 at 01:02 UTC