Enrico Tassi (Sep 23 2021 at 12:31): Enrico Tassi (Sep 23 2021 at 12:31):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.
Enrico Tassi (Sep 23 2021 at 12:31):Is this scenario (non-installed coq + coq_makefile) supported?
Emilio Jesús Gallego Arias (Sep 23 2021 at 12:37):should be Enrico, test-suite for example can run like that
Emilio Jesús Gallego Arias (Sep 23 2021 at 12:37):open an issue with the details and we can look into it
Emilio Jesús Gallego Arias (Sep 23 2021 at 12:37):the .cm are not in the same directory since a long time
Emilio Jesús Gallego Arias (Sep 23 2021 at 12:38):that's where coqcorelib points to
Enrico Tassi (Sep 23 2021 at 12:38):about that place, there was a symlink for kernel but not lib for example
Enrico Tassi (Sep 23 2021 at 12:38):the plugin in question was opening Pp from a .mlg file
Enrico Tassi (Sep 23 2021 at 12:39):and the ocamlc invokation did mention -I ..../coq-core/lib but that dir is not there, IIRC
Enrico Tassi (Sep 23 2021 at 12:39):(it was on @Yves Bertot PC, not mine)
Enrico Tassi (Sep 23 2021 at 12:40):adding by hand the symlink did not work either, because, as you say, the dir contains the .cm[x]a, but no .cmi
Enrico Tassi (Sep 23 2021 at 12:40):I did not investigate further
Enrico Tassi (Sep 23 2021 at 12:40):(since installing coq system/opam wide did fix the issue)
Last updated: Dec 06 2023 at 15:01 UTC