Stream: MetaCoq

Topic: ✔ Build errors


view this post on Zulip Jason Gross (Oct 13 2022 at 15:10):

On branch coq-8.16, I get

make -f Makefile.plugin
make[2]: Entering directory '/home/jgross/Documents/GitHub/metacoq/safechecker'
CAMLC -c src/ssrbool.mli
CAMLC -c src/pCUICPrimitive.mli
CAMLC -c src/pCUICNormal.mli
ocamlfind: Package `coq-metacoq-template-ocaml.plugin' not found
ocamlfind: Package `coq-metacoq-template-ocaml.plugin' not found
ocamlfind: Package `coq-metacoq-template-ocaml.plugin' not found
make[3]: *** [Makefile.plugin:727: src/ssrbool.cmi] Error 2
make[3]: *** [Makefile.plugin:727: src/pCUICPrimitive.cmi] Error 2
make[3]: *** [Makefile.plugin:727: src/pCUICNormal.cmi] Error 2
make[3]: Target 'real-all' not remade because of errors.
make[2]: *** [Makefile.plugin:409: all] Error 2
make[2]: Leaving directory '/home/jgross/Documents/GitHub/metacoq/safechecker'

What's up with this?

view this post on Zulip Yannick Forster (Oct 13 2022 at 15:15):

Did you do run ./configure.sh -local and make before?

view this post on Zulip Jason Gross (Oct 17 2022 at 10:44):

I ran ./configure.sh; I figured -local was only for if I wasn't planning to run make install?

view this post on Zulip Matthieu Sozeau (Oct 17 2022 at 10:50):

You need -local if you're not going to install template/pcuic/etc separately

view this post on Zulip Matthieu Sozeau (Oct 17 2022 at 10:50):

But in one go

view this post on Zulip Jason Gross (Oct 17 2022 at 10:58):

I tried running (roughly) while true; do make -k; make install -k; done and the errors never went away, IIRC?

view this post on Zulip Matthieu Sozeau (Oct 17 2022 at 11:00):

Hmm, it's easier if you just use the right config flag

view this post on Zulip Jason Gross (Oct 17 2022 at 11:01):

Do I need to make clean or something before I do ./configure -local; make?

view this post on Zulip Jason Gross (Oct 17 2022 at 11:01):

If I don't clean, I get

make[2]: Entering directory '/home/jgross/Documents/GitHub/metacoq/safechecker'
COQDEP VFILES
CAMLC -c src/ssrbool.mli
ocamlfind: Package `coq-metacoq-template-ocaml.plugin' not found
make[3]: *** [Makefile.plugin:727: src/ssrbool.cmi] Error 2
make[2]: *** [Makefile.plugin:409: all] Error 2

view this post on Zulip Matthieu Sozeau (Oct 17 2022 at 12:19):

I would git clean and ./configure.sh local

view this post on Zulip Jason Gross (Oct 18 2022 at 08:56):

Even with git clean and ./configure.sh -local, I'm getting

CAMLC -c src/pCUICNormal.mli
ocamlfind: Package `coq-metacoq-template-ocaml.plugin' not found
Command exited with non-zero status 2
src/pCUICNormal.cmi (real: 0.00, user: 0.00, sys: 0.00, mem: 4152 ko)

Maybe this is because I'm building first with make and when that fails I try again with make COQEXTRAFLAGS="-native-compiler ondemand"?

view this post on Zulip Jason Gross (Oct 18 2022 at 09:00):

Nope, now build fails with

make[2]: Leaving directory '/home/jgross/Documents/GitHub/metacoq/template-coq'
make[1]: Leaving directory '/home/jgross/Documents/GitHub/metacoq/template-coq'
make -C pcuic
make -C translations
make[1]: Entering directory '/home/jgross/Documents/GitHub/metacoq/translations'
cat metacoq-config > _CoqProject
make[1]: Entering directory '/home/jgross/Documents/GitHub/metacoq/pcuic'
make[1]: *** No rule to make target 'metacoq-config', needed by '_CoqProject'.
make[1]: Target 'all' not remade because of errors.
make[1]: Leaving directory '/home/jgross/Documents/GitHub/metacoq/pcuic'

view this post on Zulip Matthieu Sozeau (Oct 18 2022 at 09:24):

It's just local or --enable-local IIRC

view this post on Zulip Jason Gross (Oct 18 2022 at 09:36):

Ah, thanks

view this post on Zulip Jason Gross (Oct 22 2022 at 05:33):

make[2]: Entering directory '/home/jgross/Documents/GitHub/metacoq/safechecker'
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/jgross/Documents/GitHub/metacoq/safechecker/src/././metacoq_safechecker_plugin.cmxs: undefined symbol: camlMetacoq_template_plugin__Monad_utils__check_eq_true_332\")")

Any thoughts on this one?

view this post on Zulip Jason Gross (Oct 28 2022 at 17:57):

It seems that this occurs when you are trying to build with ./configure.sh local but also have a(n inconsistent) copy of MetaCoq installed...

view this post on Zulip Notification Bot (Nov 07 2022 at 23:10):

Jason Gross has marked this topic as resolved.


Last updated: Mar 02 2024 at 16:01 UTC