coq build fails

[Ryan Schmidt]

Does 8.1pl3 work better for you? Try this patch:

http://trac.macports.org/ticket/13940


On May 10, 2008, at 5:41 AM, Dimitri Hendriks wrote:

> Dear all,
>
> I tried to build the port coq, but it fails, see output below.
> Any ideas?
>
> Thanks, Dimitri
>
> diem at jarvis:~<502> sudo port install coq
> Password:
> --->  Fetching camlp5
> --->  Attempting to fetch camlp5-5.08.tgz from http:// 
> pauillac.inria.fr/~ddr/camlp5/distrib/src/
> --->  Verifying checksum(s) for camlp5
> --->  Extracting camlp5
> --->  Configuring camlp5
> --->  Building camlp5 with target world.opt
> --->  Staging camlp5 into destroot
> --->  Installing camlp5 5.08_0
> --->  Activating camlp5 5.08_0
> --->  Cleaning camlp5
> --->  Fetching coq
> Error: No defined site for tag: coq, using master_sites
> --->  Attempting to fetch coq-8.1pl2.tar.gz from http:// 
> coq.inria.fr/V8.1pl2/files/
> --->  Verifying checksum(s) for coq
> --->  Extracting coq
> --->  Configuring coq
> --->  Building coq with target world
> Error: Target org.macports.build returned: shell command " cd "/opt/ 
> local/var/macports/build/ 
> _opt_local_var_macports_sources_rsync.macports.org_release_ports_lang_ 
> coq/work/coq-8.1pl2" && make world " returned error 2
> Command output: OCAMLOPT4 contrib/recdef/recdef.ml4
> OCAMLC    contrib/funind/tacinvutils.mli
> OCAMLOPT  contrib/funind/tacinvutils.ml
> OCAMLOPT4 contrib/funind/tacinv.ml4
> OCAMLC    contrib/funind/indfun_common.mli
> OCAMLOPT  contrib/funind/indfun_common.ml
> OCAMLC    contrib/funind/rawtermops.mli
> OCAMLOPT  contrib/funind/rawtermops.ml
> OCAMLC    contrib/funind/rawterm_to_relation.mli
> OCAMLOPT  contrib/funind/rawterm_to_relation.ml
> OCAMLC    contrib/funind/functional_principles_proofs.mli
> OCAMLOPT  contrib/funind/functional_principles_proofs.ml
> OCAMLC    contrib/funind/functional_principles_types.mli
> OCAMLOPT  contrib/funind/functional_principles_types.ml
> OCAMLOPT  contrib/funind/invfun.ml
> OCAMLOPT  contrib/funind/indfun.ml
> OCAMLOPT  contrib/funind/merge.ml
> OCAMLOPT4 contrib/funind/indfun_main.ml4
> OCAMLOPT -a -o contrib/contrib.cmxa
> "gcc" -o kernel/byterun/coq_fix_code.o -fno-defer-pop -Wall -Wno- 
> unused -I "/opt/local/lib/ocaml"/caml  -c kernel/byterun/ 
> coq_fix_code.c
> "gcc" -o kernel/byterun/coq_memory.o -fno-defer-pop -Wall -Wno- 
> unused -I "/opt/local/lib/ocaml"/caml  -c kernel/byterun/coq_memory.c
> "gcc" -o kernel/byterun/coq_values.o -fno-defer-pop -Wall -Wno- 
> unused -I "/opt/local/lib/ocaml"/caml  -c kernel/byterun/coq_values.c
> "gcc" -o kernel/byterun/coq_interp.o -fno-defer-pop -Wall -Wno- 
> unused -I "/opt/local/lib/ocaml"/caml  -c kernel/byterun/coq_interp.c
> "ar" rc kernel/byterun/libcoqrun.a kernel/byterun/coq_fix_code.o  
> kernel/byterun/coq_memory.o kernel/byterun/coq_values.o kernel/ 
> byterun/coq_interp.o
> "ranlib" kernel/byterun/libcoqrun.a
> COQMKTOP -o bin/coqtop.opt
> powerpc-apple-darwin8-gcc-4.0.1: /opt/local/lib/ocaml/camlp5/ 
> gramlib.a: No such file or directory
> Error during linking
> make[1]: *** [bin/coqtop.opt] Error 2
> make: *** [world] Error 2