Stream: Coq devs & plugin devs

Topic: coq_makefile and `-devel` (post dune)


view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:31):

Is this scenario (non-installed coq + coq_makefile) supported?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 12:37):

should be Enrico, test-suite for example can run like that

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 12:37):

open an issue with the details and we can look into it

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 12:37):

the .cm are not in the same directory since a long time

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 12:38):

that's where coqcorelib points to

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:38):

about that place, there was a symlink for kernel but not lib for example

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:38):

the plugin in question was opening Pp from a .mlg file

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:39):

(it was on @Yves Bertot PC, not mine)

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:40):

I did not investigate further

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:40):

(since installing coq system/opam wide did fix the issue)


Last updated: Oct 16 2021 at 03:02 UTC