FAQ: Compilation problems - MetaRocq/metarocq GitHub Wiki

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.

• <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.