On branch coq-8.16, I get
make -f Makefile.plugin make: 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: *** [Makefile.plugin:727: src/ssrbool.cmi] Error 2 make: *** [Makefile.plugin:727: src/pCUICPrimitive.cmi] Error 2 make: *** [Makefile.plugin:727: src/pCUICNormal.cmi] Error 2 make: Target 'real-all' not remade because of errors. make: *** [Makefile.plugin:409: all] Error 2 make: Leaving directory '/home/jgross/Documents/GitHub/metacoq/safechecker'
What's up with this?
Did you do run
./configure.sh -local and
./configure.sh; I figured
-local was only for if I wasn't planning to run
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: 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: *** [Makefile.plugin:727: src/ssrbool.cmi] Error 2 make: *** [Makefile.plugin:409: all] Error 2
I would git clean and ./configure.sh local
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: Leaving directory '/home/jgross/Documents/GitHub/metacoq/template-coq' make: Leaving directory '/home/jgross/Documents/GitHub/metacoq/template-coq' make -C pcuic make -C translations make: Entering directory '/home/jgross/Documents/GitHub/metacoq/translations' cat metacoq-config > _CoqProject make: Entering directory '/home/jgross/Documents/GitHub/metacoq/pcuic' make: *** No rule to make target 'metacoq-config', needed by '_CoqProject'. make: Target 'all' not remade because of errors. make: Leaving directory '/home/jgross/Documents/GitHub/metacoq/pcuic'
make: 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...
What does it mean if I'm getting
make: *** No rule to make target 'src/pCUICWfUniverses.cmx', needed by 'src/metacoq_safechecker_plugin.cmx'.
That you need to adapt either the Pluginproject or the ml pack file
In the wiki of MetaCoq on github there is an (incomplete) compilation error list with fixes
It is incomplete in the sense that it doesn't list all error messages, so maybe not this one
But it does list all fixes, so one of them will work
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?
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
I think you probably need to add the
mli file to the
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
Oh, is this
yes, you need to touch Extraction to get ml and mli files again
Feel free to update the instructions
Last updated: Jan 30 2023 at 18:04 UTC