FAQ: Compilation problems

Problems with building .ml and .mli files

Frequent make cleanplugin in the directory you are working in is necessary, probably after every change. Sometimes it might also be necessary to do touch theories/Extraction.v to trigger generation of ml files again.

• Error: No rule to build <dir>/src/<file>.ml: The files <file>.ml and <file>.mli need to be added to the _PluginProject or _PluginProject.in file. The order of files in there is not relevant. For template-coq, the file is _PluginProject, for all other <dir>s it it _PluginProject.in.
• Dynlink error: no implementation available for <file>Findlib paths <file> (without .v ending) needs to be added to the mlpack file ./erasure/src/metacoq_erasure_plugin.mlpack, ./safechecker/src/metacoq_safechecker_plugin.mlpack, or ./template-coq/src/template_coq.mlpack
• Error: Symbol <file> not found: <file> (without .v ending) needs to be added to the mlpack file ./erasure/src/metacoq_erasure_plugin.mlpack, ./safechecker/src/metacoq_safechecker_plugin.mlpack, or ./template-coq/src/template_coq.mlpack
• Error: <file>.cmx does not exist": <file>.ml and <file>.mli have to be removed from the respective _PluginProject or _PluginProject.in file.
• Warning XX treated as error: Add XX to the CAMLFLAGS in Makefile.plugin.local
• Axiom not realised: Check the Extract Constant commands related to guard_impl in safechecker/theories/Extraction.v Likely you need to add a similar command for the unrealised axiom.

Problems with building .v files

• <file> makes inconsistent assumptions: Either you need to run make again to recompile <file>.v, or you have installed MetaCoq globally and the local installation is picking up both global and local files.