Hi. I am trying to fix MetaCoq build after a seemingly unrelated change to the Coq standard library, and I would like some help/advice. The Coq change reorganizes dependencies between files in the Coq standard library modules extracted by MetaCoq. The error message is
ocamlfind: gen-src/wf.cmx: No such file or directory which does not appear in the faq. I have regenerated _PluginProject. What should I do to fix this issue or to figure out what is going on? Thanks!
I can't tell you for sure, but having the
mli in the
_PluginProject and not mentioning
Wf in the
mlpack seems strange. You could try that. And another observation: The CI run fails with a different error message related to
It's weird if gen-src/wf.cmx is indeed not built while being in the _PluginProject...
I tried adding
Wf on its own line at the end of
template-coq.mlpack and still got the same ocamlfind error.
Would anyone be willing to give a try to fixing this? Note that you'll need the Coq changes to work on this; without them you'll get a different error.
@Jason Gross explained that I need to delete
*.cm* between editing mlpack and rebuilding; this let me make some progress. Now the error message is
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/andreser/coq/DecidableClass-instances/_build/install/default/lib/coq-core/../coq-metacoq-template-ocaml/metacoq_template_plugin.cmxs: cannot open shared object file: No such file or directory\")")
*.cm* files currently exist in that directory?
Does doing a completely clean build fix this error?
This was a clean build.
metacoq_template_plugin.cmxs does not.
Last updated: Jun 03 2023 at 18:01 UTC