Stream: Coq devs & plugin devs

Topic: Dune and vo files


view this post on Zulip Guillaume Melquiond (Feb 09 2022 at 09:25):

When I do dune build _build/default/user-contrib/Ltac2/Notations.vo, nothing happens. What is the proper way to compile a given .vo file? I tried dune build --verbose and it does tell that the file is an "actual target", so at least it recognizes it, but that is it.

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 09:26):

don't include the _build/default/ prefix
I don't know why

view this post on Zulip Guillaume Melquiond (Feb 09 2022 at 09:27):

This does not seem to change anything.

view this post on Zulip Guillaume Melquiond (Feb 09 2022 at 09:28):

Could it be that Ltac2 files are not handled by Dune?

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 09:31):

it works for me

view this post on Zulip Guillaume Melquiond (Feb 09 2022 at 09:32):

If you modify plugins/ltac2/tac2intern.ml, does it actually recompile the .vo file?

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 09:34):

ah that's broken

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 09:35):

probably since findlib

view this post on Zulip Enrico Tassi (Feb 09 2022 at 09:37):

I don't see how findlib is a problem here

view this post on Zulip Enrico Tassi (Feb 09 2022 at 09:38):

@Guillaume Melquiond check the .d file in _build for Notations.v

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 09:40):

because the digest stuff was removed

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 09:40):

see explanation at https://github.com/coq/coq/pull/11407

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 10:11):

Gaëtan Gilbert said:

don't include the _build/default/ prefix
I don't know why

You can point to install, for _build it is not included as it is ambigous in the presence of several compilation contexts

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 10:12):

I don't mean ambigous, I man private

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 10:12):

I guess the reason is to avoid people depending on the build layout too much in their command line tools

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 10:13):

Gaëtan Gilbert said:

ah that's broken

That's not good, can you open an issue?

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 10:15):

https://github.com/coq/coq/issues/15649


Last updated: Feb 05 2023 at 19:29 UTC