coq build fails

Dimitri Hendriks diem at cs.vu.nl
Sat May 10 03:41:14 PDT 2008


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_co 
q/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

Error: Status 1 encountered during processing.



More information about the macports-users mailing list