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.
don't include the _build/default/ prefix
I don't know why
This does not seem to change anything.
Could it be that Ltac2 files are not handled by Dune?
it works for me
If you modify plugins/ltac2/tac2intern.ml
, does it actually recompile the .vo
file?
ah that's broken
probably since findlib
I don't see how findlib is a problem here
@Guillaume Melquiond check the .d file in _build for Notations.v
because the digest stuff was removed
see explanation at https://github.com/coq/coq/pull/11407
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
I don't mean ambigous, I man private
I guess the reason is to avoid people depending on the build layout too much in their command line tools
Gaëtan Gilbert said:
ah that's broken
That's not good, can you open an issue?
https://github.com/coq/coq/issues/15649
Last updated: Oct 13 2024 at 01:02 UTC