diff -r eb92bebb925e -r 26118e92cd62 Admin/page/dist-content/notes_macos_darwin.content --- /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 @@ +%title% +Isabelle under Mac OS X + +%body% + +

Mac OS X is the current version +of the Macintosh operating system, installed on all new Apple computers. Because it is based on Unix, it +can run Isabelle. The new +Power Mac G5 is an excellent +Isabelle machine. Here is a screenshot +showing Proof General running in GNU Emacs.

+ +

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.

+ +

Download Isabelle to a suitable directory, as described on the download +page. +Ensure that you get files such as +polyml_ppc-darwin.tar.gz and +HOL_ppc-darwin.tar.gz rather than the _x86-linux +versions.
Install Poly/ML in a standard +place, such as /usr/local/polyml, or put polyml in the +same directory as Isabelle. Make sure you get the PPC Darwin +version from the Poly/ML download page.
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 Fink.
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 +Isabelle/INSTALL.
Install Proof General. +You may now be able to launch Proof General by typing "Isabelle" +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 MacEmacs JP or +mindlube's or Enhanced Carbon Emacs. +Visiting a theory file from Emacs will automatically launch Proof General +provided isabelle is on the search path. None of these options +support the X-Symbol package, unfortunately.

+ +

In order to get the full benefit of Proof General, you must install the X +Window System (X11) and XEmacs or +GNU Emacs.

+ +

Apple's version 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.
Some people prefer the OroborOSX +window manager. It must be used in conjunction with XFree86, which is easy to install if you use the +installer provided by the XonX project.

+ +

The easiest way to install XEmacs or GNU Emacs is via the package manager +Fink. Install the Fink package +xemacs-sumo-pkg to get the XEmacs libraries that Proof General needs +to run. To install GNU Emacs, install the package emacs21. Fink can +compile from sources, but this takes hours, so it is better to request binary +installations.

+ +

To use GNU +Emacs instead of XEmacs, you must +recompile Proof General and X-Symbol following the instructions here. Note that Proof General +incorporates its own copy of X-Symbol.

+ +

Install X11 or OroborOSX.
Install XEmacs (and its libraries), or install GNU Emacs and recompile +Proof General.
You may want to install this drag-and-drop Isabelle launcher. It is a simple hack that +invokes xemacs on any files dropped on it.