MenhirLib does not install .coq-native directories
As far as I can tell, the install
rule of coq-menhirlib/src/Makefile
does not install the .coq-native
directory. As a consequence, it is impossible to compile a file that depends on MenhirLib using a native-enabled Coq. For example, I get the following error when compiling CompCert.
COQC cparser/Parser.v
File "./cparser/.coq-native/Ncompcert_cparser_Parser.native", line 4760, characters 15-77:
4760 | ((Obj.magic (NMenhirLib_Alphabet.Construct_NMenhirLib_Alphabet_Numbered_0_1((
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module NMenhirLib_Alphabet
Error: Native compiler exited with status 2
If so, my suggestion would be:
- Add
conflicts: ["coq-native"]
to all the existing Opam packages forcoq-menhirlib
, so that it cannot be installed next to a native-enabled compiler. - Fix the
install
rule for the next release.