help installing on mac os x?

[RobNik]

Hi,

I'm trying to get Coq installed on Mac OS X, version 10.6 (Snow  
Leopard).  I don't see any binary distributions on the web site (http://www.lix.polytechnique.fr/coq/download 
), so I downloaded the source, ran "./configure", "make", and got a  
bunch of errors like this:

/var/folders/7E/7EADtPjfEMu4pw8fKXGk4k+++TI/-Tmp-/camlasmb25848.s:
714:32-bit absolute addressing is not supported for x86-64
/var/folders/7E/7EADtPjfEMu4pw8fKXGk4k+++TI/-Tmp-/camlasmb25848.s:
714:cannot do signed 4 byte relocation

Is there a binary distribution available?  Or is there a way around  
this error?

thanks,
Rob



--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Robert-322]

On Friday 25 September 2009 21:00:27 you wrote:

> Hi,
>
> I'm trying to get Coq installed on Mac OS X, version 10.6 (Snow
> Leopard).  I don't see any binary distributions on the web site
> (http://www.lix.polytechnique.fr/coq/download ), so I downloaded the
> source, ran "./configure", "make", and got a bunch of errors like this:
>
> /var/folders/7E/7EADtPjfEMu4pw8fKXGk4k+++TI/-Tmp-/camlasmb25848.s:
> 714:32-bit absolute addressing is not supported for x86-64
> /var/folders/7E/7EADtPjfEMu4pw8fKXGk4k+++TI/-Tmp-/camlasmb25848.s:
> 714:cannot do signed 4 byte relocation
>
> Is there a binary distribution available?  Or is there a way around
> this error?

You might try the following, which uses MacPorts:

http://www.cs.princeton.edu/courses/archive/fall09/cos441/coq-mac.html

This is how I build Coq on my Mac (10.4).  I've had reports that others have
had success using these instructions, but I don't have data on specific
configurations, so YMMV.  If you don't want CoqIDE, you can skip installing X11
and the gtk stuff (gtk-doc and lablgtk2).

Rob Dockins

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[RobNik]

Thanks, that worked.  I didn't follow it exactly, but I downloaded and  
compiled OCaml from scratch, then camlp5, and then Coq compiled fine.

Rob

On Sep 25, 2009, at 6:20 PM, Robert wrote:

> You might try the following, which uses MacPorts:
>
> http://www.cs.princeton.edu/courses/archive/fall09/cos441/coq-mac.html
>
> This is how I build Coq on my Mac (10.4).  I've had reports that  
> others have
> had success using these instructions, but I don't have data on  
> specific
> configurations, so YMMV.  If you don't want CoqIDE, you can skip  
> installing X11
> and the gtk stuff (gtk-doc and lablgtk2).
>
> Rob Dockins
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Robert Soule]

There is a dmg that worked for me here:

http://pauillac.inria.fr/~herbelin/coq-8.2-intel.dmg

- Robert Soule

On Fri, Sep 25, 2009 at 11:23 PM, Robert Nikander
<rob.nikander@...> wrote:

> Thanks, that worked.  I didn't follow it exactly, but I downloaded and
> compiled OCaml from scratch, then camlp5, and then Coq compiled fine.
>
> Rob
>
> On Sep 25, 2009, at 6:20 PM, Robert wrote:
>>
>> You might try the following, which uses MacPorts:
>>
>> http://www.cs.princeton.edu/courses/archive/fall09/cos441/coq-mac.html
>>
>> This is how I build Coq on my Mac (10.4).  I've had reports that others
>> have
>> had success using these instructions, but I don't have data on specific
>> configurations, so YMMV.  If you don't want CoqIDE, you can skip
>> installing X11
>> and the gtk stuff (gtk-doc and lablgtk2).
>>
>> Rob Dockins
>>
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club