|
16233
|
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>
|