Hello Dimitri. Sorry for my delay in responding. To apply patches, you download the patch from the ticket, then do something like this:
$ sudo -s $ cd `port dir coq` $ patch -p0 < /path/to/coq.diff $ port install $ exit $ But I committed the patch yesterday and closed the ticket so there's nothing you need to do now except "sudo port selfupdate" and try again. But I don't think it will help. I did not have a problem with 8.1p2 nor 8.1p3, on Mac OS X 10.4.11 on Intel or PowerPC. I see that your error is that coq can't find gramlib.a which is supposed to be provided by camlp5. I see that you installed camlp5 5.08. That's also the version I got. My camlp5 does provide that static library: $ port contents camlp5 | grep \\.a /opt/local/lib/ocaml/camlp5/camlp5.a /opt/local/lib/ocaml/camlp5/gramlib.a /opt/local/lib/ocaml/camlp5/odyl.a $ See, "gramlib.a" is there. Is it for you? If not, try just rebuilding camlp5: $ sudo port -ncuf upgrade camlp5 $ I see you're on Mac OS X 10.4.x on a PowerPC Mac. What version of Xcode and MacPorts do you have? If you have Xcode earlier than 2.4.1, please update to 2.4.1 or 2.5. Let us know what happens. -Ryan On May 17, 2008, at 3:48 PM, Dimitri Hendriks wrote: > Can anyone tell me how to apply a patch file? > > Coq 8.1pl2 doesn't install here. I want to try a patch > called coq.diff, as Ryan suggested (see below). But how > does this work? Is there a port command for it, or do I > have to do it manually? Honestly, I do not even know to > which file this patch would apply. > > Any assistence is greatly appreciated, > Dimitri > > > On 15 May 2008, at 22:45, Dimitri Hendriks wrote: > >> 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_la >>>> n >>>> g_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
