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...
Jason Gross (Dec 14 2022 at 16:00):What does it mean if I'm getting
make[2]: *** No rule to make target 'src/pCUICWfUniverses.cmx', needed by 'src/metacoq_safechecker_plugin.cmx'.
?
Yannick Forster (Dec 14 2022 at 16:01):That you need to adapt either the Pluginproject or the ml pack file
Yannick Forster (Dec 14 2022 at 16:01):In the wiki of MetaCoq on github there is an (incomplete) compilation error list with fixes
Yannick Forster (Dec 14 2022 at 16:01):It is incomplete in the sense that it doesn't list all error messages, so maybe not this one
Yannick Forster (Dec 14 2022 at 16:01):But it does list all fixes, so one of them will work
Jason Gross (Dec 14 2022 at 16:09):This file is already listed in safechecker/src/metacoq_safechecker_plugin.mlpack, but not in safechecker/_PluginProject.in. As far as I can tell, I have not changed the Requires of any file. Should files in the mlpack all be in the _PluginProject already?
Yannick Forster (Dec 14 2022 at 16:44):I would not bet on the consistency of these files amongst each other, and I don't know in which direction inclusions have to be for compilation to work
Yannick Forster (Dec 14 2022 at 16:45):I think you probably need to add the ml and mli file to the _PluginProject.in file
Jason Gross (Dec 14 2022 at 17:47):Hmm. I'll try that. In the meantime, if I do git clean -xfd safechecker/src, and then make, I get
CAMLOPT -c -for-pack Metacoq_safechecker_plugin src/g_metacoq_safechecker.ml
File "src/g_metacoq_safechecker.mlg", line 10, characters 5-15:
Error: Unbound module Extraction
Command exited with non-zero status 2
which does not seem to be listed in the FAQ of errors. Extraction is listed both in the pluginproject and in the mlpack
Jason Gross (Dec 14 2022 at 17:54):Oh, is this touch theories/Extraction.v?
Yannick Forster (Dec 15 2022 at 10:52):yes, you need to touch Extraction to get ml and mli files again
Yannick Forster (Dec 15 2022 at 10:52):Feel free to update the instructions
Last updated: Jan 30 2023 at 18:04 UTC