Stream: MetaCoq

Topic: Build errors


view this post on Zulip 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'.

?

view this post on Zulip Yannick Forster (Dec 14 2022 at 16:01):

That you need to adapt either the Pluginproject or the ml pack file

view this post on Zulip Yannick Forster (Dec 14 2022 at 16:01):

In the wiki of MetaCoq on github there is an (incomplete) compilation error list with fixes

view this post on Zulip 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

view this post on Zulip Yannick Forster (Dec 14 2022 at 16:01):

But it does list all fixes, so one of them will work

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jason Gross (Dec 14 2022 at 17:54):

Oh, is this touch theories/Extraction.v?

view this post on Zulip Yannick Forster (Dec 15 2022 at 10:52):

yes, you need to touch Extraction to get ml and mli files again

view this post on Zulip Yannick Forster (Dec 15 2022 at 10:52):

Feel free to update the instructions


Last updated: May 31 2023 at 04:01 UTC