The Coq mailing list

[Jean-Jacques Levy <jean-jacques.levy AT inria.fr>]

Le 17 juin 2011 à 17:40, Xavier Leroy a écrit :

> Hi Jean-Jacques,
> 
>> problem with coq-8.3pl2-macosx.dmg with following plugin:
>> Disk image compiled with 32-bit option, but Ssreflect plugin is
>  compiled with 64-bit. There is this Mac format for having dual
>  formats 32+64. I think it would be preferable to distribute the dual
>  version. Moreover the standard on Mac will evolve to 64-bit.
> 
> Indeed: since Mac OS 10.6 (mid-2009), 64-bit mode is the default
> option, and it takes quite a bit of hacking to even get OCaml to
> compile in 32 bits on Mac OS 10.6.  To make things worse, Apple
> changed their linker around the same time that 10.6 came out, in ways
> that break OCaml's dynamic loading of shared libraries.  So, your
> chances to load a Coq plugin in a 32-bit MacOS version of Coq are
> exactly zero.
> 
> However, it's easy to compile Coq from sources on a Mac.  Just use
> Macports or Homebrew to install ocaml, camlp5 and lablgtk2
> automatically.  Then, Coq's sources compile like a charm, coqide
> included.

that's what I did, but from standard Coq bundle, since I could not compile 
Coq 8.3pl2 from Macports. 
Seems only 8.2 is available. -JJ-

> Cheers,
> 
> - Xavier