coq build fails

[Ryan Schmidt]

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