What does it mean if I'm getting
make[2]: *** 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 Require
s 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 ml
and mli
file to the _PluginProject.in
file
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 touch theories/Extraction.v
?
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