coq build fails

[Dimitri Hendriks]

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
>>>
>>> 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_lan 
>>> 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
>