added notes for mac os
Fri, 06 May 2005 16:03:56 +0200
changeset 15935 26118e92cd62
parent 15934 eb92bebb925e
child 15936 817ac93ee786
added notes for mac os
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-content/notes_macos_darwin.content	Fri May 06 16:03:56 2005 +0200
@@ -0,0 +1,102 @@
+Isabelle under Mac OS X
+<p><a href="">Mac OS X</a> is the current version
+of the Macintosh operating system, installed on all new <a href=
+"">Apple</a> computers. Because it is based on Unix, it
+can run <a href=
+"">Isabelle</a>. The new
+<a href="">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>
+<li>Download Isabelle to a suitable directory, as described on the download
+<a href=
+Ensure that you get files such as <a href=
+<tt>polyml_ppc-darwin.tar.gz</tt></a> and <a href=
+HOL_ppc-darwin.tar.gz</tt></a> rather than the <tt>_x86-linux</tt>
+<li>Install <a href="">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=
+<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
+<li>Install <a href="">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=
+"">MacEmacs JP</a> or
+<a href="">mindlube's</a> or <a href=
+"">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>
+<p>In order to get the full benefit of Proof General, you must install the X
+Window System (X11) and <a href="">XEmacs</a> or
+<a href="">GNU Emacs</a>.</p>
+<li><a href="">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=
+window manager. It must be used in conjunction with <a href=
+"">XFree86</a>, which is easy to install if you use the
+installer provided by the <a href=
+"">XonX</a> project.</li>
+<p>The easiest way to install XEmacs or GNU Emacs is via the package manager
+<a href="">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
+<p>To use <a href="">GNU
+Emacs</a> instead of <a href="">XEmacs</a>, you must
+recompile Proof General and X-Symbol following the instructions <a href=
+"">here</a>. Note that Proof General
+incorporates its own copy of X-Symbol.</p>
+<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>
--- a/Admin/page/dist-content/packages.content	Fri May 06 15:00:08 2005 +0200
+++ b/Admin/page/dist-content/packages.content	Fri May 06 16:03:56 2005 +0200
@@ -128,12 +128,21 @@
 <A HREF="">Proof General FAQ</a> 
 for advice.
-<h3>Running Isabelle on windows</h3>
+<h3>Running Isabelle on non-unix operating systems.</h3>
-<p>For a complete system, we recommend to run some recent version of
-Solaris, Darwin, or Linux.</p>
+<p>Though Isabelle is nativly designed for Unix (e.&nbsp;g. Solaris, Linux),
+Isabelle may also run under similar &raquo;unix-like&laquo; platforms:
-<p>Though not &raquo;officially supported&laquo;, Isabelle in most
-cases should also run on Windows, using the
-<a href="">Cygwin</a> POSIX emulation layer. Here
-some <a href="notes_win_cygwin.html">notes</a> about it.</p>
+    <ul>
+        <li>Max OS X, since the Darwin kernel is a Unix kernel; see
+        <a href="notes_macos_darwin.html">installation notes for Max OS</a>.</li>
+        <li>Windows, using the <a href="">Cygwin</a>
+        POSIX emulation layer; see <a href="notes_win_cygwin.html">installation
+        notes for Cygwin/Windows</a>.</li>
+    </ul>
+<p>These installation instructions are not strictly normative, they are just
+hints contributed by Isabelle users.
+Feel free to contact us for any suggestions, corrections or improvements.</p>