Stream: Coq users

Topic: Unable to install coq-8.5.3

view this post on Zulip shaurya gupta (Aug 19 2020 at 13:57):

I'm trying to install coq-8.5.3 using opam. 

opam switch create mpri24 4.02.3
eval `opam config env`
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install -j4 coq.8.5.3

#=== ERROR while compiling coq.8.5.3 ==========================================#
# context     2.0.7 | linux/x86_64 | ocaml-base-compiler.4.02.3 | https://opam.ocaml.org#7a1de9ce
# path        ~/.opam/mpri24-coq/.opam-switch/build/coq.8.5.3
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code   2
# env-file    ~/.opam/log/coq-439749-2dea01.env
# output-file ~/.opam/log/coq-439749-2dea01.out
### output ###
# [...]
# OCAMLC    printing/ppconstrsig.mli
# OCAMLC    printing/pptacticsig.mli
# OCAMLC    printing/printmodsig.mli
# OCAMLC    printing/ppvernacsig.mli
# OCAMLC    tactics/geninterp.mli
# OCAMLC    tactics/dnet.mli
# OCAMLC    tactics/dn.mli
# make[1]: *** No rule to make target 'tactics/hipattern.ml', needed by 'tactics/hipattern.cmx'.  Stop.
# make[1]: *** Waiting for unfinished jobs....
# OCAMLC    tactics/btermdn.mli
# make[1]: Leaving directory '/home/shaurya/.opam/mpri24-coq/.opam-switch/build/coq.8.5.3'
# make: *** [Makefile:159: submake] Error 2

I get the same error with ocaml 4.05.0. How can I fix this?

view this post on Zulip Paolo Giarrusso (Aug 19 2020 at 13:58):

Does that also fail with -j1 ?

view this post on Zulip Paolo Giarrusso (Aug 19 2020 at 13:59):

(I don't know for this specific case, but I've seen a few coq releases break with parallel builds in similar ways)

view this post on Zulip Paolo Giarrusso (Aug 19 2020 at 14:00):

Also make sure that make does not try a parallel build anyway; your log shows make -j7, so you might have some opam configuration forcing parallel builds?

view this post on Zulip shaurya gupta (Aug 19 2020 at 14:07):

@Paolo Giarrusso that didn't work either

[ERROR] The compilation of coq failed at "/home/shaurya/.opam/opam-init/hooks/sandbox.sh build make -j1".

#=== ERROR while compiling coq.8.5.3 ==========================================#
# context     2.0.7 | linux/x86_64 | ocaml-base-compiler.4.02.3 | https://opam.ocaml.org#7a1de9ce
# path        ~/.opam/mpri24-coq/.opam-switch/build/coq.8.5.3
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j1
# exit-code   2
# env-file    ~/.opam/log/coq-457110-c61e7b.env
# output-file ~/.opam/log/coq-457110-c61e7b.out
### output ###
# [...]
# OCAMLOPT  tactics/geninterp.ml
# OCAMLC    tactics/dnet.mli
# OCAMLOPT  tactics/dnet.ml
# OCAMLC    tactics/dn.mli
# OCAMLOPT  tactics/dn.ml
# OCAMLC    tactics/btermdn.mli
# OCAMLOPT  tactics/btermdn.ml
# OCAMLC    tactics/tacticals.mli
# OCAMLOPT  tactics/tacticals.ml
# make[1]: *** No rule to make target 'tactics/hipattern.ml', needed by 'tactics/hipattern.cmx'.  Stop.
# make[1]: Leaving directory '/home/shaurya/.opam/mpri24-coq/.opam-switch/build/coq.8.5.3'
# make: *** [Makefile:159: submake] Error 2

view this post on Zulip Karl Palmskog (Aug 19 2020 at 14:12):

camlp5 7.01 is known to work with 8.5.3, so you may want to make sure you're using that version of camlp5

view this post on Zulip Karl Palmskog (Aug 19 2020 at 14:12):

I think the opam package bound allows camlp5 versions that don't work

view this post on Zulip shaurya gupta (Aug 19 2020 at 14:21):

@Karl Palmskog I installed 7.01 but still the same error.

Last updated: Oct 03 2023 at 21:01 UTC