Admin/website/dist/installation.html
changeset 16233 e634d33deb86
child 16238 c1102cdf601f
equal deleted inserted replaced
16232:8a12e11d222b 16233:e634d33deb86
       
     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>