Stream: MetaCoq

Topic: stdlib-shims and compilation in _build_ci


view this post on Zulip Pierre Rousselin (Oct 20 2023 at 08:45):

Sorry for the technical (and probably stupid) question. I am trying to patch metacoq for https://github.com/coq/coq/pull/18164.
I'm in the coq repo, in _build_ci/metacoq and compilation fails, after some time with this:

W: This Makefile was generated by Coq 8.16.0
W: while the current Coq version is 8.19+alpha
CAMLC -c src/ssrbool.mli
ocamlfind: Package `stdlib-shims' not found
Command exited with non-zero status 2

the COQBIN environment variable is set and the opam switch has stdlib-shims.

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 08:49):

what commands did you run? something like make world && make ci-metacoq?

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 08:50):

and what is coqbin set to?

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 08:53):

Yes I ran this command.

~/depots/coq (rm_arith_files)$ echo $COQBIN
/home/pierre/depots/coq/_build/install/default/bin/

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 09:07):

make ci-metacoq is what produces the error?

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 09:24):

Yes. not immediately


Last updated: Jul 23 2024 at 19:02 UTC