Stream: MetaCoq

Topic: Build errors


view this post on Zulip 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?

view this post on Zulip Yannick Forster (Oct 13 2022 at 15:15):

Did you do run ./configure.sh -local and make before?

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Oct 17 2022 at 10:50):

You need -local if you're not going to install template/pcuic/etc separately

view this post on Zulip Matthieu Sozeau (Oct 17 2022 at 10:50):

But in one go

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Oct 17 2022 at 11:00):

Hmm, it's easier if you just use the right config flag

view this post on Zulip Jason Gross (Oct 17 2022 at 11:01):

Do I need to make clean or something before I do ./configure -local; make?

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 17 2022 at 12:19):

I would git clean and ./configure.sh local

view this post on Zulip 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"?

view this post on Zulip 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'

view this post on Zulip Matthieu Sozeau (Oct 18 2022 at 09:24):

It's just local or --enable-local IIRC

view this post on Zulip Jason Gross (Oct 18 2022 at 09:36):

Ah, thanks

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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'.

?

view this post on Zulip Yannick Forster (Dec 14 2022 at 16:01):

That you need to adapt either the Pluginproject or the ml pack file

view this post on Zulip Yannick Forster (Dec 14 2022 at 16:01):

In the wiki of MetaCoq on github there is an (incomplete) compilation error list with fixes

view this post on Zulip 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

view this post on Zulip Yannick Forster (Dec 14 2022 at 16:01):

But it does list all fixes, so one of them will work

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jason Gross (Dec 14 2022 at 17:54):

Oh, is this touch theories/Extraction.v?

view this post on Zulip Yannick Forster (Dec 15 2022 at 10:52):

yes, you need to touch Extraction to get ml and mli files again

view this post on Zulip Yannick Forster (Dec 15 2022 at 10:52):

Feel free to update the instructions


Last updated: Jan 30 2023 at 18:04 UTC