Stream: Dune devs & users

Topic: variable coq:version and nix


view this post on Zulip Enrico Tassi (Jan 31 2024 at 20:35):

As per https://github.com/coq-community/vscoq/pull/702 it seems that the variable works in opam- but not in nix (dune 3.13 on both CI jobs). Is there a known problem with nix and this feature? Maybe dune searches coqc in a PATH and nix juggles with it?

view this post on Zulip Enrico Tassi (Jan 31 2024 at 20:35):

CC @Vincent Laporte @Romain Tetley

view this post on Zulip Enrico Tassi (Jan 31 2024 at 20:36):

See here for the variable use in a dune file: https://github.com/coq-community/vscoq/pull/702/files#diff-18adb004de3326664416635552a77deb87167fb788ff944959d5f6270d494e25

view this post on Zulip Romain Tetley (Jan 31 2024 at 20:39):

Weirdly enough, if I type nix develop everything works fine... If I add nix develop .#vscoq-language-server, it no longer finds coqc ?

view this post on Zulip Romain Tetley (Jan 31 2024 at 20:40):

coincidently the ci uses the latter

view this post on Zulip Romain Tetley (Jan 31 2024 at 20:42):

for reference this is the flake file: https://github.com/coq-community/vscoq/blob/88787744dafe9a3305128cd0f41223ece56bc1aa/flake.nix

view this post on Zulip Romain Tetley (Jan 31 2024 at 20:42):

maybe there is a subtle difference that I don't get between the two commands ?

view this post on Zulip Vincent Laporte (Feb 01 2024 at 04:37):

I’m not aware of any known issue. How is it supposed to work?

view this post on Zulip Romain Tetley (Feb 01 2024 at 07:07):

So the only place I explicitly reference coq is in the vscoq-language-server build inputs. I don't get why if I ask to launch a shell specifically with nix develop .#vscoq-language-server which to the best of my knowledge specifies I want the dependencies from vscoq-language-server in the file I do not get coqc in my env, but I do if I only type nix develop ?

view this post on Zulip Romain Tetley (Feb 01 2024 at 14:11):

Maybe @Cyril Cohen has an idea ?

view this post on Zulip Cyril Cohen (Feb 01 2024 at 17:04):

Well, if you want nix develop .#vscoq-language-server to work, according to the manual, you need to define an output: devShells."<system>".vscoq-language-server

view this post on Zulip Cyril Cohen (Feb 01 2024 at 17:04):

which you can alias to devShells."<system>".v.default if you want

view this post on Zulip Cyril Cohen (Feb 01 2024 at 17:06):

not sure if nix develop .#name defaults to packages."<system>".name :shrug:


Last updated: May 25 2024 at 19:02 UTC