%title%
Isabelle under Mac OS X
%body%
<p><a href="http://www.apple.com/macosx/">Mac OS X</a> is the current version
of the Macintosh operating system, installed on all new <a href=
"http://www.apple.com/">Apple</a> computers. Because it is based on Unix, it
can run <a href=
"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">Isabelle</a>. The new
<a href="http://www.apple.com/powermac/">Power Mac G5</a> is an excellent
Isabelle machine. Here is a <a href="isabelle_macos_screenshot.jpg">screenshot</a>
showing Proof General running in GNU Emacs.</p>
<p>This page gives advice on building Isabelle for Mac OS X. It assumes that
you are familiar with both Mac OS X and Unix. You must have installed the Mac
OS X developer tools.</p>
<ol>
<li>Download Isabelle to a suitable directory, as described on the download
<a href=
"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/packages.html">page</a>.
Ensure that you get files such as <a href=
"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/contrib/polyml_ppc-darwin.tar.gz">
<tt>polyml_ppc-darwin.tar.gz</tt></a> and <a href=
"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/HOL_ppc-darwin.tar.gz"><tt>
HOL_ppc-darwin.tar.gz</tt></a> rather than the <tt>_x86-linux</tt>
versions.</li>
<li>Install <a href="http://www.polyml.org/">Poly/ML</a> in a standard
place, such as <tt>/usr/local/polyml</tt>, or put <tt>polyml</tt> in the
same directory as <tt>Isabelle</tt>. Make sure you get the PPC Darwin
version from the Poly/ML download page.</li>
<li>You may have to install the bash shell. Versions of Mac OS X prior to
10.2.2 did not provide it. If /bin/bash does not exist, you can install it
using the package manager <a href=
"http://fink.sourceforge.net/">Fink</a>.</li>
<li>At this point, you should be able to run Isabelle with the command line
interface. You can also build Isabelle from the Unix command line,
following the instructions for "Compiling Logics" in file
<tt>Isabelle/INSTALL.</tt></li>
<li>Install <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
You may now be able to launch Proof General by typing "<tt>Isabelle</tt>"
at the Unix command line. This will invoke the Apple-supplied version of
Emacs in a terminal window, providing a primitive environment. Somewhat
better is to run Proof General from within a version of Emacs ported as a
native Mac OS X application, such as <a href=
"http://home.att.ne.jp/alpha/z123/emacs-mac-e.html">MacEmacs JP</a> or
<a href="http://mindlube.com/products/emacs/">mindlube's</a> or <a href=
"http://www.cs.man.ac.uk/%7efranconi/mac-emacs/">Enhanced Carbon Emacs</a>.
Visiting a theory file from Emacs will automatically launch Proof General
provided <tt>isabelle</tt> is on the search path. None of these options
support the X-Symbol package, unfortunately.</li>
</ol>
<p>In order to get the full benefit of Proof General, you must install the X
Window System (X11) and <a href="http://www.xemacs.org/">XEmacs</a> or
<a href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs</a>.</p>
<ul>
<li><a href="http://www.apple.com/macosx/x11/">Apple's version</a> of X11
is included with the Panther (MacOS 10.3) installation discs, though it is
not installed by default. The Command key serves as Meta, but it is
reserved for standard Apple shortcuts such as C, V and X, so you must use
Esc-C, Esc-V and Esc-X in Emacs or else deselect "Enable key equivalents"
in the X11 preferences.</li>
<li>Some people prefer the <a href=
"http://www.osxgnu.org/software/Xwin/WindowManagers/OroborOSX/">OroborOSX</a>
window manager. It must be used in conjunction with <a href=
"http://xfree86.org/">XFree86</a>, which is easy to install if you use the
installer provided by the <a href=
"http://sourceforge.net/projects/xonx/">XonX</a> project.</li>
</ul>
<p>The easiest way to install XEmacs or GNU Emacs is via the package manager
<a href="http://fink.sourceforge.net/">Fink</a>. Install the Fink package
<tt>xemacs-sumo-pkg</tt> to get the XEmacs libraries that Proof General needs
to run. To install GNU Emacs, install the package <tt>emacs21</tt>. Fink can
compile from sources, but this takes hours, so it is better to request binary
installations.</p>
<p>To use <a href="http://www.gnu.org/software/emacs/emacs.html">GNU
Emacs</a> instead of <a href="http://www.xemacs.org/">XEmacs</a>, you must
recompile Proof General and X-Symbol following the instructions <a href=
"http://proofgeneral.inf.ed.ac.uk/FAQ">here</a>. Note that Proof General
incorporates its own copy of X-Symbol.</p>
<ol>
<li>Install X11 or OroborOSX.</li>
<li>Install XEmacs (and its libraries), or install GNU Emacs and recompile
Proof General.</li>
<li>You may want to install this drag-and-drop <a href=
"IsabelleDroplet.dmg">Isabelle launcher</a>. It is a simple hack that
invokes xemacs on any files dropped on it.</li>
</ol>