Dan Connolly (Sep 15 2021 at 04:13): Dan Connolly (Sep 15 2021 at 04:13):I'm trying to write a parser. I'm familiar with combinator parsing, so coq-parsec looked like a place to start. But I'm struggling to figure out how to "build on the shoulders of giants" around here.
I installed coq-8.13.2, but then:
$ opam install coq-parsec
The following dependencies couldn't be met:
- coq-parsec → coq >= 8.12~
no matching version
No solution found, exiting
I tried to clone and make coq-parsec, but then I get library ExtLib.Applicative is required and has not been found in the loadpath!
Dan Connolly (Sep 15 2021 at 04:15):I have a mild preference for using nix but opam is ok too. I have ceres downloaded and compiled... how do I get coq-parsec to find it?
Guillaume Melquiond (Sep 15 2021 at 07:02):I tried it locally and Opam was able to find a solution: coq 8.13.2, coq-ext-lib 0.11.3, coq-ceres 0.4.0, coq-parsec 0.1.0. So, my guess is that one of those libraries cannot be installed due to some other constraints (e.g., unrelated libraries) and Opam's error message is just misleading about the cause of the conflict.
Karl Palmskog (Sep 15 2021 at 07:37):based on the error message, it appears the Coq registered in opam is not 8.13.2. Would recommend doing opam switch and opam list and checking that 8.13.2 is really installed and activated in the current switch.
Ana de Almeida Borges (Sep 15 2021 at 11:57):I don't know whether it's relevant here, but this kind of error can also occur when the OCaml version itself is not compatible with one of the dependencies. In that case it's kind of hard to figure out, so I leave it here as an investigation avenue.
Théo Zimmermann (Sep 15 2021 at 12:02):For a Nix-based solution, see https://github.com/NixOS/nixpkgs/pull/137999.
Karl Palmskog (Sep 15 2021 at 12:18):none of the dependencies of coq-parsec (including itself) have any specific OCaml bounds, as far as I can see.
Guillaume Melquiond (Sep 15 2021 at 12:27):I do not know why you are talking about bounds on OCaml, but note that there might be some by transitivity. For example, installing coq-parsec might force an upgrade of coq-ext-lib, which in turn forces an upgrade of coq-quickchick, which has bounds on OCaml.
Dan Connolly (Sep 15 2021 at 22:11):the 8.13.2 that I installed was from nix, so maybe nix and opam are not getting along well
Dan Connolly (Sep 15 2021 at 22:14):Theo, did you cook that up just for me? thanks!
Théo Zimmermann (Sep 16 2021 at 06:55):Dan Connolly said:
the 8.13.2 that I installed was from nix, so maybe nix and opam are not getting along well
More generally, opam doesn't support using a system-wide installed Coq unfortunately :frown:
Théo Zimmermann (Sep 16 2021 at 06:58):Dan Connolly said:
Theo, did you cook that up just for me? thanks!
Yes, with the recent introduction of the mkCoqDerivation, adding new Coq packages to nixpkgs is rather straightforward (as you can see in the PR diff) and documented at https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq. Having the opam files to know about the version constraints is also helpful.
Karl Palmskog (Sep 16 2021 at 07:00):More generally, opam doesn't support using a system-wide installed Coq unfortunately :(
My take: you can have a system Coq just fine, as long as the opam Coq has priority in your PATH. And you will have to adjust your PATH to get the system Coq
Théo Zimmermann (Sep 16 2021 at 07:10):What I meant is that unfortunately installing a Coq package with opam requires recompiling Coq with opam. It will not be able to use the system-wide installed Coq like it would be able to do for OCaml.
Karl Palmskog (Sep 16 2021 at 07:12):OK, sure, I agree that they can't be mixed in that sense.
Guillaume Melquiond (Sep 16 2021 at 07:21):You can always execute opam install --fake coq. Later, you would also need to run sudo opam install coq-parsec later on, so that files can be installed in write-protected locations.
Théo Zimmermann (Sep 16 2021 at 07:24):That might work with a typical system-wide installed Coq, but definitely not with a Nix-installed one since its install directory would be read-only.
Théo Zimmermann (Sep 16 2021 at 07:24):And wouldn't be as flexible as opam being able to install packages in a local switch while depending on a system-wide OCaml.
Guillaume Melquiond (Sep 16 2021 at 07:30):I guess you could always type unionsfs somewhere/in/my/home:path/to/coq/theories just after opam install --fake. Or am I misunderstanding the issue?
Théo Zimmermann (Sep 16 2021 at 07:33):Maybe. I had never heard of unionfs before. The usual approach when installing Coq packages with Nix is rather to extend the COQPATH environment variable.
Guillaume Melquiond (Sep 16 2021 at 07:35):Isn't Nix itself using union mounts? I thought this was the underlying technology?
Théo Zimmermann (Sep 16 2021 at 08:08):I could be mistaken but I don't think so.
Guillaume Melquiond (Sep 16 2021 at 09:27):Indeed, my mistake. I thought the /etc directory was handled through union mounts; but no, these are just symlinks. (Apparently, union mounts were the preferred design, but it ended up being impossible due to a bad interaction between ZFS and union mounts.)
Paolo Giarrusso (Sep 16 2021 at 19:00):@Guillaume Melquiond How safe is sudo opam install… today? are the package scripts still sandboxed?
Paolo Giarrusso (Sep 16 2021 at 19:03):in any case, based on lots of requests for help, most users should follow @Théo Zimmermann ‘s tip and not mix different Coq installs, unless they have the background needed to keep them straight (say, they are comfortable with opam switches or Nix)
Paolo Giarrusso (Sep 16 2021 at 19:05):I’ve seen enough people try opam install coq-foo on a non-opam-installed Coq (last example: https://coq.discourse.group/t/ask-for-basic-commands-for-coq/1418/16). Maybe it’s a general issue somehow.
Théo Zimmermann (Sep 16 2021 at 19:50):Maybe it would deserve a Stack Overflow question if there is not already one...
Last updated: Oct 03 2023 at 04:02 UTC