Jason Gross (Oct 13 2022 at 15:10): 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?
Yannick Forster (Oct 13 2022 at 15:15):Did you do run ./configure.sh -local and make before?
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?
Matthieu Sozeau (Oct 17 2022 at 10:50):You need -local if you're not going to install template/pcuic/etc separately
Matthieu Sozeau (Oct 17 2022 at 10:50):But in one go
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?
Matthieu Sozeau (Oct 17 2022 at 11:00):Hmm, it's easier if you just use the right config flag
Jason Gross (Oct 17 2022 at 11:01):Do I need to make clean or something before I do ./configure -local; make?
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
I would git clean and ./configure.sh local
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"?
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'
It's just local or --enable-local IIRC
Jason Gross (Oct 18 2022 at 09:36):Ah, thanks
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?
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...
Notification Bot (Nov 07 2022 at 23:10):Jason Gross has marked this topic as resolved.
Last updated: Jun 01 2023 at 12:01 UTC