coq build fails

[Dimitri Hendriks]

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