What does it mean if I'm getting
make: *** No rule to make target 'src/pCUICWfUniverses.cmx', needed by 'src/metacoq_safechecker_plugin.cmx'.
That you need to adapt either the Pluginproject or the ml pack file
In the wiki of MetaCoq on github there is an (incomplete) compilation error list with fixes
It is incomplete in the sense that it doesn't list all error messages, so maybe not this one
But it does list all fixes, so one of them will work
This file is already listed in safechecker/src/metacoq_safechecker_plugin.mlpack, but not in safechecker/_PluginProject.in. As far as I can tell, I have not changed the
Requires of any file. Should files in the mlpack all be in the _PluginProject already?
I would not bet on the consistency of these files amongst each other, and I don't know in which direction inclusions have to be for compilation to work
I think you probably need to add the
mli file to the
Hmm. I'll try that. In the meantime, if I do
git clean -xfd safechecker/src, and then
make, I get
CAMLOPT -c -for-pack Metacoq_safechecker_plugin src/g_metacoq_safechecker.ml File "src/g_metacoq_safechecker.mlg", line 10, characters 5-15: Error: Unbound module Extraction Command exited with non-zero status 2
which does not seem to be listed in the FAQ of errors.
Extraction is listed both in the pluginproject and in the mlpack
Oh, is this
yes, you need to touch Extraction to get ml and mli files again
Feel free to update the instructions
Last updated: May 31 2023 at 04:01 UTC