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?
Did you do run ./configure.sh -local
and make
before?
I ran ./configure.sh
; I figured -local
was only for if I wasn't planning to run make install
?
You need -local if you're not going to install template/pcuic/etc separately
But in one go
I tried running (roughly) while true; do make -k; make install -k; done
and the errors never went away, IIRC?
Hmm, it's easier if you just use the right config flag
Do I need to make clean
or something before I do ./configure -local; make
?
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
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"
?
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
Ah, thanks
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?
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...
Jason Gross has marked this topic as resolved.
Last updated: Jun 01 2023 at 12:01 UTC