Stream: Coq devs & plugin devs

Topic: Installation issue (Unbound module Vernactypes)


view this post on Zulip Quentin VERMANDE (Oct 30 2023 at 09:41):

Hi. I need to install Coq from source, however, when I subsequently try to compile coq-elpi, I have an Unbound module Vernactypes error. I have first tried installing Coq with make world and adding .../_build/default/bin to my PATH, and I also tried the quick install suggested by make help-install (adding coqide-server, as it is a dependency of coq-elpi). In the second case, I confirmed that coq-core was added to the expected lib directory and that coq-core/vernac contained vernactypes.ml. Am I missing something obvious?

view this post on Zulip Gaëtan Gilbert (Oct 30 2023 at 09:45):

this is the stuff we set for local builds of the ci- targets https://github.com/coq/coq/blob/9e891cf7b24a1b220ffb24deb1aec51207fe3943/dev/ci/ci-common.sh#L33-L36

view this post on Zulip Quentin VERMANDE (Oct 30 2023 at 10:18):

Thank you. I did a fresh make worldinstall and set OCAMLPATH, COQBIN, COQLIB, COQCORELIB and PATH to their corresponding directory in _build/default. Now I have Unbond module CClosure.RedFlags... Also, now I have a warning from findlib complaining that Package coq-core hase multiple definitions, the second one being from an opam switch that should be inactive and that does not appear in any of my environment variables, so I am completely lost.

view this post on Zulip Gaëtan Gilbert (Oct 30 2023 at 10:26):

CClosure.RedFlags doesn't exist in master, sounds like you have an outdated plugin

view this post on Zulip Quentin VERMANDE (Oct 30 2023 at 10:48):

Thank you again, I made progress by checking out the v8.18 branch. Now I have Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/quentin/.opam/coq8.18/lib/coq-core/plugins/ltac/ltac_plugin.cmxs: undefined symbol: camlLocusops__10\")") (with a lot of findlib warnings as mentioned above). The active opam switch is not coq8.18 and env | grep coq8 prints nothing, so I have no idea how this cmxs file is found (and I do not understand the error either).

view this post on Zulip Paolo Giarrusso (Oct 30 2023 at 12:48):

did you undo the original global install?
IIRC findlib has state outside the environment — including auto-discovered META files and findlib.conf.

view this post on Zulip Paolo Giarrusso (Oct 30 2023 at 12:52):

_and_ if you're using a _system_ ocaml compiler, that adds state shared across the switches — and that can be mutable, tho if you're lucky mutation will require sudo.

view this post on Zulip Quentin VERMANDE (Oct 30 2023 at 13:12):

Yes, I removed the switch (which I had used as prefix for dune) and started from scratch.
I indeed have a system ocaml compiler... Is there a way to force the right files to be used?

view this post on Zulip Paolo Giarrusso (Oct 30 2023 at 13:39):

The quickest test might be reinstalling the system compiler, and ideally check if uninstall removes everything or leaves debris from the manual install.

view this post on Zulip Paolo Giarrusso (Oct 30 2023 at 13:43):

I'm under-qualified for more careful troubleshooting, but I wonder if libraries might have been installed among the system libraries next to the system compiler

view this post on Zulip Paolo Giarrusso (Oct 30 2023 at 13:47):

That theory assumes the switch uses the system compiler intentionally, or your PATH shadows the one from opam (shell extensions don't really compose), and/or you forgot eval $(opam env) at some crucial point

view this post on Zulip Paolo Giarrusso (Oct 30 2023 at 13:48):

(but there's no specific evidence for the last beyond "we're humans")


Last updated: Oct 13 2024 at 01:02 UTC