FAQ: Compilation problems

Problems with building .ml and .mli files

• Error: No rule to build <dir>/gen-src/<file>.ml: The files <file>.ml and <file>.mli need to be added to the _PluginProject or _PluginProject 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.
• 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" -> .mland.mlihave to be *removed* from the resepectve_PluginProjector_PluginProject.in` file.

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.