coq build fails

Dimitri Hendriks diem at cs.vu.nl
Sun May 18 15:20:51 PDT 2008 

Hi Ryan, thanks a lot for your response!

I did a selfupdate (but thanks for showing how to patch!),
and tried again to install coq, but resuls in the same error
about the missing file gramlib.a.

Indeed, I do not have this file gramlib.a.
I reinstalled campl5, but this does not
bring gramlib.a ! See output below.

I am on a Mac 10.4.11, PPC. I have Xcode version 2.5
and macports 1.600.

Thanks,
Dimitri

diem at jarvis:~<503> port contents camlp5 | grep \\.a
   /opt/local/lib/ocaml/camlp5/camlp5.a
   /opt/local/lib/ocaml/camlp5/odyl.a
diem at jarvis:~<504> sudo port -ncuf upgrade camlp5
Password:
--->  Fetching camlp5
--->  Verifying checksum(s) for camlp5
--->  Extracting camlp5
--->  Configuring camlp5
--->  Building camlp5 with target world.opt
--->  Staging camlp5 into destroot
--->  Deactivating camlp5 5.08_0
--->  Uninstalling camlp5 5.08_0
--->  Installing camlp5 5.08_0
--->  Activating camlp5 5.08_0
--->  Cleaning camlp5
diem at jarvis:~<505> port contents camlp5 | grep *.a
diem at jarvis:~<506> port contents camlp5 | grep \\.a
   /opt/local/lib/ocaml/camlp5/camlp5.a
   /opt/local/lib/ocaml/camlp5/odyl.a
diem at jarvis:~<507>



On 18 May 2008, at 01:46, Ryan Schmidt wrote:

> 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_l 
>>>>> an
>>>>> 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

More information about the macports-users mailing list