|
1 <?xml version='1.0' encoding='iso-8859-1' ?> |
|
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
3 <?cvs id="$Id$"?> |
|
4 <html xmlns="http://www.w3.org/1999/xhtml"> |
|
5 |
|
6 <head> |
|
7 <title>Installation instructions</title> |
|
8 <?include file="//include/htmlheader.include.html"?> |
|
9 </head> |
|
10 |
|
11 <body class="dist"> |
|
12 <?include file="//include/header.include.html"?> |
|
13 <div class="hr"><hr/></div> |
|
14 <?include file="//include/navigation_dist.include.html"?> |
|
15 <div class="hr"><hr/></div> |
|
16 <div id="content"> |
|
17 |
|
18 <h2>Prerequisites</h2> |
|
19 |
|
20 <p>Isabelle runs on common Unix platforms (Linux, Solaris, etc.). |
|
21 Below we provide also some <a href="#other_platforms">hints</a> |
|
22 on how to use Isabelle on other, not-quite-Unix platforms.</p> |
|
23 |
|
24 <p> |
|
25 The packages available from our <a href="download.html">download page</a> |
|
26 expect the following software to be installed: |
|
27 </p> |
|
28 |
|
29 <ul> |
|
30 <li>bash 1.x or 2.x</li> |
|
31 <li>Perl 5.x</li> |
|
32 <li>optionally, XEmacs 21 or Emacs 21 with mule support (for ProofGeneral)</li> |
|
33 <li>optionally, Java 1.1 or above (for theory graph browsing)</li> |
|
34 </ul> |
|
35 |
|
36 <p> |
|
37 Our download page includes packages for a suitable implementation of Standard ML |
|
38 (<a href="http://www.polyml.org">Poly/ML</a>) and |
|
39 <a |
|
40 href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> |
|
41 (please <a |
|
42 href="http://proofgeneral.inf.ed.ac.uk/register">register</a>). The |
|
43 Proof General distribution now already includes the <a |
|
44 href="http://x-symbol.sourceforge.net">X-Symbol</a> package, |
|
45 there is no need to download it separately. |
|
46 </p> |
|
47 |
|
48 <h2>Installation</h2> |
|
49 |
|
50 <p>In fact, there is no |
|
51 installation required. Users may just unpack all required packages within the |
|
52 same directory. The default settings of Isabelle should be reasonable for |
|
53 most circumstances.</p> |
|
54 |
|
55 <p>A typical Linux/x86 site installation of Isabelle/HOL works as follows:</p> |
|
56 <ul> |
|
57 <li>By using GNU <tt>tar</tt>, the archives are uncompressed and unpacked into the |
|
58 <tt>/usr/local</tt> directory (this location may be changed to anything |
|
59 appropriate): |
|
60 <blockquote> |
|
61 <tt>tar -C /usr/local -xzf <?value key="distname"?>.tar.gz</tt><br /> |
|
62 <tt>tar -C /usr/local -xzf ProofGeneral.tar.gz</tt><br /> |
|
63 <tt>tar -C /usr/local -xzf polyml_base.tar.gz</tt><br /> |
|
64 <tt>tar -C /usr/local -xzf polyml_x86-linux.tar.gz</tt><br /> |
|
65 <tt>tar -C /usr/local -xzf HOL_x86-linux.tar.gz</tt><br /> |
|
66 </blockquote> |
|
67 </li> |
|
68 <li> |
|
69 Users may now invoke Isabelle without further ado, e.g. run the main |
|
70 executable <tt>/usr/local/Isabelle/bin/Isabelle</tt> to launch the Proof |
|
71 General interface for Isabelle/Isar. Note that there is a separate option in |
|
72 the Proof General <em>Options</em> menu to enable X-Symbol. |
|
73 </li> |
|
74 <li>If Emacs appears to hang when the prover process is started, see the |
|
75 <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for |
|
76 advice. |
|
77 </li> |
|
78 </ul> |
|
79 |
|
80 <p>For more information, see the file <a href="../isabelle/Isabelle/INSTALL">INSTALL</a> included in |
|
81 <?value key="distname"?>.tar.gz.</p> |
|
82 |
|
83 <h2 id="other_platforms">Other platforms</h2> |
|
84 |
|
85 <p>Although Isabelle is natively designed for Unix environments, |
|
86 it may also run under similar, Unix-like platforms. The |
|
87 following installation instructions are hints contributed by |
|
88 Isabelle users. Please feel free to contact us for any suggestions, |
|
89 corrections or improvements.</p> |
|
90 |
|
91 <ul> |
|
92 <li><a href="installation_notes_macosx.html">Installation notes for Mac OS |
|
93 X</a></li> |
|
94 |
|
95 <li><a href="installation_notes_cygwin.html">Installation notes for |
|
96 Cygwin/Windows</a></li> |
|
97 </ul> |
|
98 |
|
99 </div> |
|
100 <div class="hr"><hr/></div> |
|
101 <?include file="../include/footer.include.html"?> |
|
102 </body> |
|
103 |
|
104 </html> |