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...
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'.
?
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 Require
s 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 ml
and mli
file to the _PluginProject.in
file
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 touch theories/Extraction.v
?
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