The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

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.

Cheers,

- Xavier