--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/installation_notes_macosx.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,120 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Installation hints for Mac OS X</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>Installing on Mac OS X</h2>
+ <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=
+ "../img/screenshot_isabelle_macos.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
+
+ <ul>
+ <li><?value key="distname"?>.tar.gz</li>
+ <li>ProofGeneral.tar.gz</li>
+ <li>polyml_base.tar.gz</li>
+ <li>polyml_ppc-darwin.tar.gz</li>
+ <li>HOL_ppc-darwin.tar.gz</li>
+ </ul>
+ </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>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="../include/footer.include.html"?>
+</body>
+
+</html>