1 <?xml version='1.0' encoding='iso-8859-1' ?> |
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"> |
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$"?> |
3 <!-- $Id$ --> |
4 <html xmlns="http://www.w3.org/1999/xhtml"> |
4 <html xmlns="http://www.w3.org/1999/xhtml"> |
5 |
5 |
6 <head> |
6 <head> |
7 <title>Installation instructions</title> |
7 <title>Installation instructions</title> |
8 <?include file="//include/htmlheader.include.html"?> |
8 <?include file="//include/htmlheader.include.html"?> |
52 same directory. The default settings of Isabelle should be reasonable for |
52 same directory. The default settings of Isabelle should be reasonable for |
53 most circumstances.</p> |
53 most circumstances.</p> |
54 |
54 |
55 <p>A typical Linux/x86 site installation of Isabelle/HOL works as follows:</p> |
55 <p>A typical Linux/x86 site installation of Isabelle/HOL works as follows:</p> |
56 <ul> |
56 <ul> |
57 <li>By using GNU <tt>tar</tt>, the archives are uncompressed and unpacked into the |
57 <li>By using GNU <tt class="shellcmd">tar</tt>, the archives are uncompressed and unpacked into the |
58 <tt>/usr/local</tt> directory (this location may be changed to anything |
58 <tt class="shellcmd">/usr/local</tt> directory (this location may be changed to anything |
59 appropriate): |
59 appropriate): |
60 <blockquote> |
60 <ul class="shellcmd"> |
61 <tt>tar -C /usr/local -xzf <?value key="distname"?>.tar.gz</tt><br /> |
61 <li>tar -C /usr/local -xzf <?value key="distname"?>.tar.gz</li> |
62 <tt>tar -C /usr/local -xzf ProofGeneral.tar.gz</tt><br /> |
62 <li>tar -C /usr/local -xzf ProofGeneral.tar.gz</li> |
63 <tt>tar -C /usr/local -xzf polyml_base.tar.gz</tt><br /> |
63 <li>tar -C /usr/local -xzf polyml_base.tar.gz</li> |
64 <tt>tar -C /usr/local -xzf polyml_x86-linux.tar.gz</tt><br /> |
64 <li>tar -C /usr/local -xzf polyml_x86-linux.tar.gz</li> |
65 <tt>tar -C /usr/local -xzf HOL_x86-linux.tar.gz</tt><br /> |
65 <li>tar -C /usr/local -xzf HOL_x86-linux.tar.gz</li> |
66 </blockquote> |
66 </ul> |
67 </li> |
67 </li> |
68 <li> |
68 <li> |
69 Users may now invoke Isabelle without further ado, e.g. run the main |
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 |
70 executable <tt class="shellcmd">/usr/local/Isabelle/bin/Isabelle</tt> to launch the Proof |
71 General interface for Isabelle/Isar. Note that there is a separate option in |
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. |
72 the Proof General <em>Options</em> menu to enable X-Symbol. |
73 </li> |
73 </li> |
74 <li>If Emacs appears to hang when the prover process is started, see the |
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 |
75 <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for |