README.html
author webertj
Mon Mar 07 19:17:07 2005 +0100 (2005-03-07)
changeset 15582 7219facb3fd0
parent 15278 25dc2f17661b
child 16327 cd2cd49e6c8f
permissions -rw-r--r--
HTML 4.01 Transitional conformity
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <!-- $Id$ -->
     4 
     5 <html>
     6 
     7 <head>
     8   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     9   <title>The Isabelle System Distribution</title>
    10 </head>
    11 
    12 <body>
    13 
    14 <h1>The Isabelle System Distribution</h1>
    15 
    16 <h2>Version information</h2>
    17 
    18 This is the internal repository version of Isabelle.  See the
    19 <tt>NEWS</tt> file in the distribution for details on user-relevant
    20 changes.
    21 
    22 
    23 <h2>System requirements</h2>
    24 
    25 Isabelle requires a real Unix box with sufficient resources, say 64 MB
    26 of free main memory and a decent CPU.  Speaking by today's hardware
    27 standards, any moderate Linux box should give a very nice platform for
    28 Isabelle.
    29 
    30 <p>
    31 
    32 Furthermore, Isabelle needs the following software, which is not part
    33 of the distribution:
    34 <ul>
    35 <li>A full Standard ML Compiler (e.g. Poly/ML).
    36 <li>The GNU bash shell (version 1.x or 2.x).
    37 <li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
    38 is <em>not</em> sufficient).
    39 </ul>
    40 
    41 <p>
    42 
    43 The following ML system and platform combinations are known to work
    44 very well:
    45 <ul>
    46 <li>Poly/ML 4.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.
    47 <li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
    48 </ul>
    49 
    50 <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
    51 commercial product, is back in the free world.  It is by far the best
    52 compiler for running Isabelle, requiring the least memory and offering
    53 the highest performance.
    54 
    55 <p> <a href="http://smlnj.sourceforge.net/">SML/NJ</a> needs more
    56 store and disk space, but on the other hand supports more platforms.
    57 The current official release is 110.
    58 
    59 
    60 <h2>Installation</h2>
    61 
    62 Binary packages are available for Isabelle/HOL and ZF for several
    63 platforms from the Isabelle web page.  The system may be easily built
    64 from scratch as well, taking the traditional tar.gz source
    65 distribution.  See file <tt>INSTALL</tt> as distributed with Isabelle
    66 for more information.
    67 
    68 Further background information may be found in the <em>Isabelle System
    69 Manual</em>, distributed with the sources (directory <tt>doc</tt>).
    70 
    71 
    72 <h2>User interface</h2>
    73 
    74 The canonical Isabelle user interface is <a
    75 href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by David Aspinall
    76 and others.  It is a generic (X)Emacs interface for proof assistants,
    77 including Isabelle (both for the classic and Isar version).  Proof
    78 General is suitable for use by pacifists and Emacs militants
    79 alike. Its most prominent feature is script management, providing a
    80 metaphor of <em>live proof script editing</em>.  Proof General has
    81 recently gained a rather large following of both beginning and expert
    82 users of Isabelle.
    83 
    84 <p>
    85 
    86 Proof General is distributed together with the XEmacs
    87 <a href="http://x-symbol.sourceforge.net">
    88 X-Symbol package</a>, which provides a nice way to get proper
    89 mathematical symbols displayed on screen.
    90 
    91 
    92 <h2>Other sources of information</h2>
    93 
    94 <h3>The Isabelle Page</h3>
    95 
    96 The Isabelle home page may be accessed both from Cambridge and Munich:
    97 
    98 <ul>
    99 
   100 <li><a
   101 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
   102 
   103 <li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
   104 
   105 </ul>
   106 
   107 
   108 <h3>Mailing list</h3>
   109 
   110 The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
   111 provides a forum for Isabelle users to discuss problems and exchange
   112 information. To join, send a message to <a
   113 href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.
   114 
   115 
   116 <h3>Personal mail</h3>
   117 
   118 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
   119 Computer Laboratory<br>
   120 University of Cambridge<br>
   121 JJ Thomson Avenue<br>
   122 Cambridge CB3 0FD<br>
   123 England<br>
   124 <br>
   125 E-mail: <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A><br>
   126 Phone: +44-223-763500<br>
   127 Fax:   +44-223-334748<br>
   128 
   129 <p>
   130 or
   131 <p>
   132 
   133 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
   134 Institut fr Informatik<br>
   135 Technische Universit´┐Ż Mnchen<br>
   136 Boltzmannstr. 3<br>
   137 D-85748 Garching<br>
   138 Germany<br>
   139 <br>
   140 E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>
   141 Phone: +49-89-289-17302<br>
   142 Fax:   +49-89-289-17307<br>
   143 <p>
   144 
   145 <hr>
   146 
   147 Please report any problems you encounter.  While we shall try to be
   148 helpful, we can accept no responsibility for the deficiencies of
   149 Isabelle and their consequences.
   150 
   151 <hr>
   152 
   153 </body>
   154 </html>