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
[EMAIL PROTECTED]:~<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
_______________________________________________
macports-users mailing list
[email protected]
http://lists.macosforge.org/mailman/listinfo/macports-users
