Thanks for your reply! Sorry for my ignorance, but what do I have to do with this file coq.diff ?
Thanks, Dimitri On 11 May 2008, at 03:49, Ryan Schmidt wrote: > 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.cgi/macports-users
