Building Coq trunk + native CoqIDE under Mac OS X

This is done under 10.6 using macports, the whole compilation processes can take several hours.

CoqIDE (native)

We are going to compile a version of GTK that uses native rendering so we don't need X11.app.

If you've already installed cairo, pango, gtk or any of the packages below, and they are not of the +no_x11 and +quartz variant, you need to "port uninstall" them first.

So, to get started:

sudo bash
port install cairo +no_x11 +quartz
port install pango +no_x11
port install gtk2 +no_x11 +quartz
port install libgnomui +no_x11
port install ocaml
port install camlp5
port install lablgtk2

(For math-classes or corn you also need port install scons).

Then, as of 1.5.2011, the ige-mac-integration package is broken but easily fixed. The checksums fail, probably because the developer replaced the archives without bumping the version number or notifying macports.

In any case, in /opt/local/var/macports/sources/rsync.macports.org/release/ports/devel/ige-mac-integration/

open Portfile, and modify the checksums to read:

checksums       md5     56eca21af5ac5ef39cf306f08c11ea8c \
                sha1    235ee6915299340dc7a4ea301996521be99e7eef \
                rmd160  0a2bcf4f7125b7b0ed2255ec41d94df18b91f6e9

So install that, port install ige-mac-integration.

Then, in the coq-trunk checkout, ./configure -opt -local and make it. You can then start the Coq IDE bin/coqide!

However, I my case coqide complained about missing locales:

(process:25614): Gtk-WARNING **: Locale not supported by C library.
    Using the fallback 'C' locale.

This is a problem as the 'C' localse doesn't support unicode, and a lot of our source uses unicode symbols.

My locale settings look like:

LANG=
LC_COLLATE="C"
LC_CTYPE="en_US.UTF-8"
LC_MESSAGES="C"
LC_MONETARY="C"
LC_NUMERIC="C"
LC_TIME="C"
LC_ALL=

Running locale -a shows me all installed locales, and the en_US.UTF-8 is amongst them!?.

I don't really understand what the problem is. In any case, one this that works for me is:

export LC_ALL="en_US.UTF-8"

This automatically overrides all other locale settings:

LANG=
LC_COLLATE="en_US.UTF-8"
LC_CTYPE="en_US.UTF-8"
LC_MESSAGES="en_US.UTF-8"
LC_MONETARY="en_US.UTF-8"
LC_NUMERIC="en_US.UTF-8"
LC_TIME="en_US.UTF-8"
LC_ALL="en_US.UTF-8"

Then coqide just works. There is one final problem, fonts!

Install either Dejavu Sans or Freefont, we use proportional fonts.

Enjoy!

TODO: unicode input