1 %title% |
|
2 Isabelle under Mac OS X |
|
3 |
|
4 %body% |
|
5 |
|
6 <p><a href="http://www.apple.com/macosx/">Mac OS X</a> is the current version |
|
7 of the Macintosh operating system, installed on all new <a href= |
|
8 "http://www.apple.com/">Apple</a> computers. Because it is based on Unix, it |
|
9 can run <a href= |
|
10 "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">Isabelle</a>. The new |
|
11 <a href="http://www.apple.com/powermac/">Power Mac G5</a> is an excellent |
|
12 Isabelle machine. Here is a <a href="isabelle_macos_screenshot.jpg">screenshot</a> |
|
13 showing Proof General running in GNU Emacs.</p> |
|
14 |
|
15 <p>This page gives advice on building Isabelle for Mac OS X. It assumes that |
|
16 you are familiar with both Mac OS X and Unix. You must have installed the Mac |
|
17 OS X developer tools.</p> |
|
18 |
|
19 <ol> |
|
20 <li>Download Isabelle to a suitable directory, as described on the |
|
21 <a href="packages.html">download page</a>. Be sure to get the following files |
|
22 |
|
23 <ul> |
|
24 <li><tt><!-- _GP_ href(distname . ".tar.gz", distname . ".tar.gz") --></tt></li> |
|
25 <li><tt><!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --></tt></li> |
|
26 <li><tt><!-- _GP_ href("contrib/polyml_base.tar.gz", "polyml_base.tar.gz") --></tt></li> |
|
27 <li><tt><!-- _GP_ href("contrib/polyml_ppc-darwin.tar.gz", "polyml_ppc-darwin.tar.gz") --></tt></li> |
|
28 <li><tt><!-- _GP_ href("HOL_ppc-darwin.tar.gz", "HOL_ppc-darwin.tar.gz") --></tt></li> |
|
29 </ul> |
|
30 </li> |
|
31 |
|
32 <li>You may have to install the bash shell. Versions of Mac OS X prior to |
|
33 10.2.2 did not provide it. If /bin/bash does not exist, you can install it |
|
34 using the package manager <a href= |
|
35 "http://fink.sourceforge.net/">Fink</a>.</li> |
|
36 |
|
37 <li>At this point, you should be able to run Isabelle with the command line |
|
38 interface. You can also build Isabelle from the Unix command line, |
|
39 following the instructions for "Compiling Logics" in file |
|
40 <tt>Isabelle/INSTALL.</tt></li> |
|
41 |
|
42 <li>You should also be able to launch <a |
|
43 href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by typing |
|
44 "<tt>Isabelle</tt>" at the Unix command line. This will invoke the |
|
45 Apple-supplied version of Emacs in a terminal window, providing a |
|
46 primitive environment. Somewhat better is to run Proof General from |
|
47 within a version of Emacs ported as a native Mac OS X application, |
|
48 such as <a href= |
|
49 "http://home.att.ne.jp/alpha/z123/emacs-mac-e.html">MacEmacs JP</a> or |
|
50 <a href="http://mindlube.com/products/emacs/">mindlube's</a> or <a |
|
51 href= "http://www.cs.man.ac.uk/%7efranconi/mac-emacs/">Enhanced Carbon |
|
52 Emacs</a>. Visiting a theory file from Emacs will automatically |
|
53 launch Proof General provided <tt>isabelle</tt> is on the search |
|
54 path. None of these options support the X-Symbol package, |
|
55 unfortunately.</li> </ol> |
|
56 |
|
57 <p>In order to get the full benefit of Proof General, you must install the X |
|
58 Window System (X11) and <a href="http://www.xemacs.org/">XEmacs</a> or |
|
59 <a href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs</a>.</p> |
|
60 |
|
61 <ul> |
|
62 <li><a href="http://www.apple.com/macosx/x11/">Apple's version</a> of X11 |
|
63 is included with the Panther (MacOS 10.3) installation discs, though it is |
|
64 not installed by default. The Command key serves as Meta, but it is |
|
65 reserved for standard Apple shortcuts such as C, V and X, so you must use |
|
66 Esc-C, Esc-V and Esc-X in Emacs or else deselect "Enable key equivalents" |
|
67 in the X11 preferences.</li> |
|
68 |
|
69 <li>Some people prefer the <a href= |
|
70 "http://www.osxgnu.org/software/Xwin/WindowManagers/OroborOSX/">OroborOSX</a> |
|
71 window manager. It must be used in conjunction with <a href= |
|
72 "http://xfree86.org/">XFree86</a>, which is easy to install if you use the |
|
73 installer provided by the <a href= |
|
74 "http://sourceforge.net/projects/xonx/">XonX</a> project.</li> |
|
75 </ul> |
|
76 |
|
77 <p>The easiest way to install XEmacs or GNU Emacs is via the package manager |
|
78 <a href="http://fink.sourceforge.net/">Fink</a>. Install the Fink package |
|
79 <tt>xemacs-sumo-pkg</tt> to get the XEmacs libraries that Proof General needs |
|
80 to run. To install GNU Emacs, install the package <tt>emacs21</tt>. Fink can |
|
81 compile from sources, but this takes hours, so it is better to request binary |
|
82 installations.</p> |
|
83 |
|
84 <p>To use <a href="http://www.gnu.org/software/emacs/emacs.html">GNU |
|
85 Emacs</a> instead of <a href="http://www.xemacs.org/">XEmacs</a>, you must |
|
86 recompile Proof General and X-Symbol following the instructions <a href= |
|
87 "http://proofgeneral.inf.ed.ac.uk/FAQ">here</a>. Note that Proof General |
|
88 incorporates its own copy of X-Symbol.</p> |
|
89 |
|
90 <ol> |
|
91 <li>Install X11 or OroborOSX.</li> |
|
92 |
|
93 <li>Install XEmacs (and its libraries), or install GNU Emacs and recompile |
|
94 Proof General.</li> |
|
95 |
|
96 <li>You may want to install this drag-and-drop <a href= |
|
97 "IsabelleDroplet.dmg">Isabelle launcher</a>. It is a simple hack that |
|
98 invokes xemacs on any files dropped on it.</li> |
|
99 </ol> |
|
100 |
|