Jason Gross (Dec 14 2022 at 16:00): Jason Gross (Dec 14 2022 at 16:00):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'.
?
Yannick Forster (Dec 14 2022 at 16:01):That you need to adapt either the Pluginproject or the ml pack file
Yannick Forster (Dec 14 2022 at 16:01):In the wiki of MetaCoq on github there is an (incomplete) compilation error list with fixes
Yannick Forster (Dec 14 2022 at 16:01):It is incomplete in the sense that it doesn't list all error messages, so maybe not this one
Yannick Forster (Dec 14 2022 at 16:01):But it does list all fixes, so one of them will work
Jason Gross (Dec 14 2022 at 16:09):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?
Yannick Forster (Dec 14 2022 at 16:44):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
Yannick Forster (Dec 14 2022 at 16:45):I think you probably need to add the ml and mli file to the _PluginProject.in file
Jason Gross (Dec 14 2022 at 17:47):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
Jason Gross (Dec 14 2022 at 17:54):Oh, is this touch theories/Extraction.v?
Yannick Forster (Dec 15 2022 at 10:52):yes, you need to touch Extraction to get ml and mli files again
Yannick Forster (Dec 15 2022 at 10:52):Feel free to update the instructions
Last updated: May 31 2023 at 04:01 UTC