Build fails with "undefined symbol: camlMetacoq_template_plugin__Primitive__7"

[haansn08]

I run into a problem when building MetaCoq 1.1 for Coq 8.16 from the source release. The full error is:

COQC theories/Loader.v
File "./theories/Loader.v", line 4, characters 0-51:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/dev/metacoq-1.1-8.16/safechecker/src/././metacoq_safechecker_plugin.cmxs: undefined symbol: camlMetacoq_template_plugin__Primitive__7\")")

metacoq-compile-log.txt

I'm quite lost at how to solve this problem.

[yforster]

I think the problem is that you have MetaCoq installed as an opam package and want to build locally. That's what the

findlib: [WARNING] Package coq-metacoq-template-ocaml has multiple definitions in /home/dev/metacoq-1.1-8.16/safechecker/../template-coq/META.coq-metacoq-template-ocaml, /home/dev/.local/share/ocaml/coq-metacoq-template-ocaml/META

warnings are about.

Try getting rid of anything MetaCoq-related in /home/dev/.local/share/ocaml/, then build locally, and then -- optionally -- use make install to install again.

[haansn08]

@yforster I do not use opam, but I did have an compiled version of MetaCoq in my path indeed. Removing the old files indeed gets rid of the warnings, but I still get the same compilation error: metacoq-error.txt

[JasonGross]

This should be added to the FAQ of compilation problems