%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
<a href="packages.html">download page</a>. Be sure to get the following files
<!-- _GP_ href(distname . ".tar.gz", distname . ".tar.gz") --> <br>
<!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --> <br>
<!-- _GP_ href("contrib/polyml_base.tar.gz", "polyml_base.tar.gz") --> <br>
<!-- _GP_ href("contrib/polyml_ppc-darwin.tar.gz", "polyml_ppc-darwin.tar.gz") --> <br>
<!-- _GP_ href("HOL_ppc-darwin.tar.gz", "HOL_ppc-darwin.tar.gz") --> <br>
</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>You should also be able to launch <a
href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> 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>