Andres Erbsen (Jan 13 2023 at 03:56): Andres Erbsen (Jan 13 2023 at 03:56):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!
Yannick Forster (Jan 13 2023 at 08:23):I can't tell you for sure, but having the ml and 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 gen-src/decidableClass.ml
Matthieu Sozeau (Jan 13 2023 at 12:42):It's weird if gen-src/wf.cmx is indeed not built while being in the _PluginProject...
Andres Erbsen (Jan 13 2023 at 19:42):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.
Andres Erbsen (Jan 17 2023 at 14:52):@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\")")
Jason Gross (Jan 17 2023 at 14:54):Do any *.cm* files currently exist in that directory?
Does doing a completely clean build fix this error?
Andres Erbsen (Jan 17 2023 at 14:58):This was a clean build. metacoq_template_plugin.cmx exists, metacoq_template_plugin.cmxs does not.
Last updated: Jun 03 2023 at 18:01 UTC