Apparently if you compile coq by hand with profile devel then coq_makefile spits in the conf file of the generated makefile a path like .../_build_vo/...
and that one contains .vo
but not the .cm*
used to compile .ml*
files.
Is this scenario (non-installed coq + coq_makefile) supported?
should be Enrico, test-suite for example can run like that
open an issue with the details and we can look into it
the .cm are not in the same directory since a long time
that's where coqcorelib points to
about that place, there was a symlink for kernel
but not lib
for example
the plugin in question was opening Pp
from a .mlg
file
and the ocamlc invokation did mention -I ..../coq-core/lib
but that dir is not there, IIRC
(it was on @Yves Bertot PC, not mine)
adding by hand the symlink did not work either, because, as you say, the dir contains the .cm[x]a, but no .cmi
I did not investigate further
(since installing coq system/opam wide did fix the issue)
Last updated: Jun 04 2023 at 19:30 UTC