Stream: Nix toolbox devs & users

Topic: ✔ 404 for coq archive


view this post on Zulip Ali Caglayan (Jun 07 2023 at 12:04):

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.

view this post on Zulip Théo Zimmermann (Jun 07 2023 at 12:39):

Pierre Roux said:

I guess mathcomp = "2.0" should be mathcomp = "2.0.0" and maybe coq = "8.17" should be coq = "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.

view this post on Zulip Théo Zimmermann (Jun 07 2023 at 12:41):

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.

view this post on Zulip Théo Zimmermann (Jun 07 2023 at 12:45):

Oops, I hadn't seen that Cyril had already replied with the same information.

view this post on Zulip Pierre Jouvelot (Jun 07 2023 at 12:45):

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

view this post on Zulip Notification Bot (Jun 07 2023 at 12:45):

Pierre Jouvelot has marked this topic as resolved.

view this post on Zulip Cyril Cohen (Jun 07 2023 at 13:00):

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.

view this post on Zulip Ali Caglayan (Jun 07 2023 at 13:06):

If you are having trouble finding dune in nixpkgs, it is named dune_3


Last updated: Oct 13 2024 at 01:02 UTC