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?
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
Thank you. I did a fresh make world
install 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.
CClosure.RedFlags doesn't exist in master, sounds like you have an outdated plugin
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).
did you undo the original global install?
IIRC findlib
has state outside the environment — including auto-discovered META
files and findlib.conf
.
_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
.
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?
The quickest test might be reinstalling the system compiler, and ideally check if uninstall removes everything or leaves debris from the manual install.
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
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
(but there's no specific evidence for the last beyond "we're humans")
Last updated: Oct 13 2024 at 01:02 UTC