updated;
authorwenzelm
Fri May 05 22:23:27 2000 +0200 (2000-05-05)
changeset 880985539b33be03
parent 8808 204f4ebbba64
child 8810 d0eae42f6d12
updated;
INSTALL
README.html
     1.1 --- a/INSTALL	Fri May 05 22:18:40 2000 +0200
     1.2 +++ b/INSTALL	Fri May 05 22:23:27 2000 +0200
     1.3 @@ -1,67 +1,148 @@
     1.4  
     1.5 -Isabelle compilation and installation notes
     1.6 +Isabelle installation and compilation notes
     1.7  ===========================================
     1.8  
     1.9 -Unpacking the archive
    1.10 ----------------------
    1.11 +1) User installation
    1.12 +--------------------
    1.13 +
    1.14 +Here we assume that Isabelle has already been installed at your site.
    1.15 +Otherwise see 2) below of how to get the Isabelle system installed in
    1.16 +the first place.
    1.17 +
    1.18 +
    1.19 +1a) Running the Isabelle binaries
    1.20 +---------------------------------
    1.21 +
    1.22 +The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
    1.23 +directly from their location within the distribution directory
    1.24 +[ISABELLE_HOME] like this:
    1.25 +
    1.26 +  [ISABELLE_HOME]/bin/isabelle HOL
    1.27 +
    1.28 +This starts an interactive Isabelle session within your current text
    1.29 +terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
    1.30 +search PATH, but this is not strictly necessary.
    1.31 +
    1.32 +
    1.33 +Please do *not* copy (or link) the Isabelle scripts anywhere else ---
    1.34 +they just won't work!  If you really want to install independent
    1.35 +Isabelle binaries somewhere else then do it like this:
    1.36 +
    1.37 +  [ISABELLE_HOME]/bin/isatool install -p ~/bin
    1.38  
    1.39 -After unpacking the Isabelle distribution archive (using tar and gzip)
    1.40 -you are left with some directory IsabelleYY-X. You may install this
    1.41 -anywhere, but please just *not* as ~/isabelle!!!
    1.42 +Your site-wide Isabelle installation may already provide Isabelle
    1.43 +executables in some global bin directory (such as /usr/bin).
    1.44 +
    1.45 +
    1.46 +1b) Isabelle as KDE application
    1.47 +-------------------------------
    1.48 +
    1.49 +Isabelle may be installed as application icon on the KDE desktop like
    1.50 +this:
    1.51 +
    1.52 +  [ISABELLE_HOME]/bin/isatool install -k
    1.53  
    1.54 -The place where you put the contents of IsabelleYY-X will be referred
    1.55 -to as [ISABELLE_HOME] subsequently.
    1.56 +Clicking on that icon will invoke the interface wrapper script
    1.57 +(capital Isabelle), which may be configured to run your favorite
    1.58 +Isabelle user interface via the ISABELLE_INTERFACE setting.
    1.59 +Additional options may be passed by editing the application's command
    1.60 +line (by using the standard KDE desktop functionality).
    1.61 +
    1.62 +
    1.63 +2) System installation
    1.64 +----------------------
    1.65 +
    1.66 +The Isabelle distribution is available both as traditional source-only
    1.67 +tar.gz archives, and as binary packages (currently only RPM for
    1.68 +Linux/x86).  In any case, the resulting Isabelle installation always
    1.69 +contains the full sources, thus any part of the system be recompiled
    1.70 +later, too.
    1.71  
    1.72  
    1.73 -Auto configuration
    1.74 +2a) Binary installation
    1.75 +----------------------
    1.76 +
    1.77 +Ready-to-go RPM packages are provided for the ML compiler and runtime
    1.78 +system, the Isabelle sources, and some major object-logics.  These
    1.79 +packages should work on any major RPM-based Linux/x86 platform (such
    1.80 +as SuSE, RedHat etc.).  A typical installation procedure would be like
    1.81 +this (executed as root):
    1.82 +
    1.83 +  rpm -i smlnj-110.0-3.i386.rpm
    1.84 +  rpm -i --prefix /usr/share isabelle.rpm
    1.85 +  rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
    1.86 +
    1.87 +The install prefix may be changed as indicated.  By default the ML
    1.88 +system is expected to be at the same directory level as Isabelle
    1.89 +itself; changing this arrangement requires
    1.90 +[ISABELLE_HOME]/etc/settings to be adapted manually.
    1.91 +
    1.92 +
    1.93 +Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
    1.94 +Isabelle as platform independent sources.  Precompiled object-logics
    1.95 +are provided for convenience.
    1.96 +
    1.97 +
    1.98 +Recompiling logics
    1.99  ------------------
   1.100  
   1.101 -There are some minor adaptions to be made of the Isabelle distribution
   1.102 -to your system environment. Simply type:
   1.103 +Some people prefer to be able to reconstruct the full system from the
   1.104 +sources, rather than installing RPM packages blindly.  We do not
   1.105 +provide source RPMs, yet any parts of Isabelle may be recompiled after
   1.106 +installation of the main isabelle.rpm package (which contains only
   1.107 +sources anyway).
   1.108 +
   1.109 +Assuming proper configuration of the underlying ML system, Isabelle
   1.110 +object-logics may be recompiled like this:
   1.111 +
   1.112 +  [ISABELLE_HOME]/build HOL FOL
   1.113 +
   1.114 +
   1.115 +Source installation
   1.116 +-------------------
   1.117 +
   1.118 +Traditional tar.gz archives are provided for the full Isabelle sources
   1.119 +and documentation as well.  Make sure your ML system (SML/NJ, Poly/ML
   1.120 +etc.) has already been installed properly; then proceed as follows.
   1.121 +
   1.122 +
   1.123 +* Unpacking the archives.  After unpacking the Isabelle distribution
   1.124 +archives (using tar and gzip) you are left with some directory
   1.125 +IsabelleYY-X.  Basically, this may be installed anywhere --- just note
   1.126 +that ~/isabelle would be a really bad idea, though.  The place where
   1.127 +you put the contents of IsabelleYY-X will be referred to as
   1.128 +[ISABELLE_HOME] subsequently.
   1.129 +
   1.130 +
   1.131 +* Auto configuration.  There are some minor adaptions to be made of
   1.132 +the Isabelle distribution to your system environment (mostly locations
   1.133 +of bash and perl).  Simply do it like this:
   1.134  
   1.135    cd [ISABELLE_HOME]
   1.136    ./configure
   1.137  
   1.138 -This does not store any references to [ISABELLE_HOME]. You may safely
   1.139 -move the system later, without running ./configure again.
   1.140 +Note that this does not store any references to [ISABELLE_HOME].  You
   1.141 +may safely move the system later, without having to run ./configure
   1.142 +again.
   1.143  
   1.144  
   1.145 -ML system settings and compilation
   1.146 -----------------------------------
   1.147 -
   1.148 -Before actual compilation you have to tell Isabelle about your
   1.149 -Standard ML system.  These settings reside in ./etc/settings, which
   1.150 -may be also overridden by ~/isabelle/etc/settings. There are already
   1.151 -various sample configurations in ./etc/settings commented out.
   1.152 +* ML system settings and compilation.  Before actual compilation you
   1.153 +have to tell Isabelle about your Standard ML system.  These settings
   1.154 +reside in ./etc/settings, which may be also overridden by
   1.155 +~/isabelle/etc/settings. There are already various sample
   1.156 +configurations in ./etc/settings commented out.
   1.157  
   1.158  To build the core Isabelle/Pure and the default object-logic, just
   1.159 -type:
   1.160 +type
   1.161  
   1.162    ./build
   1.163  
   1.164 -More object-logics can be made similarly:
   1.165 +More object-logics can be made in a similar fashion:
   1.166  
   1.167    ./build FOL HOL
   1.168  
   1.169 -
   1.170 -Running the system
   1.171 -------------------
   1.172 -
   1.173 -Provided that compilation was successful, you can now run something
   1.174 -like:
   1.175 -
   1.176 -  [ISABELLE_HOME]/bin/isabelle FOL
   1.177 -
   1.178 -This starts an interactive Isabelle session within your current text
   1.179 -terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
   1.180 -search PATH.
   1.181 -
   1.182 -Please do *not* copy (or link) the Isabelle scripts anywhere else, or
   1.183 -they just won't work!  If you really feel the urge to install
   1.184 -independent Isabelle binaries anywhere else do it like this:
   1.185 -
   1.186 -  [ISABELLE_HOME]/bin/isatool install -p /usr/local/bin
   1.187 -
   1.188 +After successful compilation you are ready to run the system, see 1)
   1.189 +above for more information.
   1.190  
   1.191  
   1.192  $Id$
     2.1 --- a/README.html	Fri May 05 22:18:40 2000 +0200
     2.2 +++ b/README.html	Fri May 05 22:23:27 2000 +0200
     2.3 @@ -1,4 +1,3 @@
     2.4 -
     2.5  <html>
     2.6  
     2.7  <!-- $Id$ -->
     2.8 @@ -25,7 +24,7 @@
     2.9  starts at about 32-64 MB of free main memory (somewhat depending on
    2.10  your ML system), with several tens of MB disk space and a decent CPU.
    2.11  Speaking by today's hardware standards, any moderate Linux box should
    2.12 -make a nice platform for Isabelle.
    2.13 +give a very nice platform for Isabelle.
    2.14  
    2.15  <p>
    2.16  
    2.17 @@ -43,38 +42,38 @@
    2.18  The following ML system and platform combinations are known to work
    2.19  very well:
    2.20  <ul>
    2.21 -<li> Poly/ML 3.x on Linux and Suns.
    2.22 -<li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns).
    2.23 +<li> Poly/ML 3.x on Linux and Sparc/Solaris.
    2.24 +<li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
    2.25  <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    2.26  problems with Linux and HP-UX, though.
    2.27  </ul>
    2.28  
    2.29 -<p> <A HREF="http://www.polyml.org/">Poly/ML</A>, previously a commercial
    2.30 -product, is back in the public domain.  It is the best compiler for running
    2.31 -Isabelle, requiring the least memory and offering the fastest performance.
    2.32 +<p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
    2.33 +commercial product, is back in the free world.  It is by far the best
    2.34 +compiler for running Isabelle, requiring the least memory and offering
    2.35 +the highest performance.
    2.36  
    2.37  <p> <a
    2.38  href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
    2.39 -needs lots of store and disk space, but it is free.  The current
    2.40 -official release is 110 (there is an <a
    2.41 -href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM
    2.42 -archive</a> available for Linux/x86).  We still support the old 0.93
    2.43 -release, but do not recommend it.
    2.44 +needs lots of store and disk space, but supports many more platforms.
    2.45 +The current official release is 110.  Basically, we still support the
    2.46 +old 0.93 release, but do not recommend it.
    2.47  
    2.48 -<p> MLWorks is a commercial ML programming environment developed by 
    2.49 -<a href="http://www.harlequin.com/">Harlequin</A> and was
    2.50 -unfortunately withdrawn after that company was taken over.  Isabelle on
    2.51 -MLWorks 2.0 works well.  It is about 20% faster than on SML/NJ while using
    2.52 -slightly less memory and disk space.  A few minor features (e.g. ML top-level
    2.53 -pretty printing) are not supported, though. 
    2.54 -
    2.55 +<p> MLWorks is a commercial ML programming environment developed by <a
    2.56 +href="http://www.harlequin.com/">Harlequin</a> and was unfortunately
    2.57 +withdrawn after that company was taken over.  Isabelle on MLWorks 2.0
    2.58 +works well.  It is about 20% faster than on SML/NJ while using
    2.59 +slightly less memory and disk space.  A few minor features (e.g. ML
    2.60 +top-level pretty printing) are not supported, though.
    2.61  
    2.62  
    2.63  <h2>Installation</h2>
    2.64  
    2.65 -Binary rpm packages are available for Isabelle/HOL and ZF on the
    2.66 -Linux/x86 platform.  Alternatively, the system may be built from
    2.67 -scratch as described in file <tt>INSTALL</tt> of the Isabelle sources.
    2.68 +RPM packages are available for Isabelle/HOL and ZF on the Linux/x86
    2.69 +platform.  The system may be easily built from scratch as well, taking
    2.70 +the traditional tar.gz distribution.  See file <tt>INSTALL</tt> as
    2.71 +distributed with Isabelle for more information.
    2.72 +
    2.73  Further background information may be found in the <em>Isabelle System
    2.74  Manual</em>, distributed with the sources (directory <tt>doc</tt>).
    2.75  
    2.76 @@ -82,33 +81,51 @@
    2.77  <h2>User interfaces</h2>
    2.78  
    2.79  The distribution includes only a very primitive interface based on
    2.80 -ordinary terminal sessions. Advanced interfaces are available from 
    2.81 +ordinary terminal sessions. Advanced interfaces are available from
    2.82  other sources:
    2.83  
    2.84 -<UL>
    2.85 -<LI>
    2.86 -<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
    2.87 -David Aspinall is a more elaborate interface for Isabelle.  It runs
    2.88 -under recent versions of XEmacs and is useful to both novices and
    2.89 -experts.
    2.90 +<ul>
    2.91  
    2.92 -<LI>
    2.93 -<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> is
    2.94 -a generic Emacs interface for proof assistants, including Isabelle
    2.95 -(both for the classic and Isar version).  Proof General is suitable
    2.96 -for use by pacifists and Emacs militants alike. Its most prominent
    2.97 -feature is script management, providing a metaphor of <em>live proof
    2.98 -script editing</em>.
    2.99 -</UL>
   2.100 +<li>
   2.101 +<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
   2.102 +David Aspinall and others is a generic Emacs interface for proof
   2.103 +assistants, including Isabelle (both for the classic and Isar
   2.104 +version).  Proof General is suitable for use by pacifists and Emacs
   2.105 +militants alike. Its most prominent feature is script management,
   2.106 +providing a metaphor of <em>live proof script editing</em>.  Proof
   2.107 +General has recently gained a rather large following of both beginning
   2.108 +and expert users of Isabelle.
   2.109 +
   2.110 +<li>
   2.111 +<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
   2.112 +David Aspinall is an older and simpler Emacs interface for Isabelle.
   2.113 +It runs under recent versions of XEmacs.
   2.114 +
   2.115 +</ul>
   2.116 +
   2.117  
   2.118  <h2>Other sources of information</h2>
   2.119  
   2.120 +<h3>The Isabelle Page</h3>
   2.121 +
   2.122 +The Isabelle home page may be accessed both from Cambridge and Munich:
   2.123 +
   2.124 +<ul>
   2.125 +
   2.126 +<li> <a
   2.127 +href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
   2.128 +
   2.129 +<li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
   2.130 +
   2.131 +</ul>
   2.132 +
   2.133 +
   2.134  <h3>Mailing list</h3>
   2.135  
   2.136 -The electronic mailing list <TT>isabelle-users@cl.cam.ac.uk</TT>
   2.137 +The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
   2.138  provides a forum for Isabelle users to discuss problems and exchange
   2.139 -information. To join, send a message to
   2.140 -<A HREF="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</A>.
   2.141 +information. To join, send a message to <a
   2.142 +href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.
   2.143  
   2.144  
   2.145  <h3>Personal mail</h3>
   2.146 @@ -130,7 +147,7 @@
   2.147  
   2.148  <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
   2.149  Institut fuer Informatik<br>
   2.150 -T. U. Muenchen<br>	
   2.151 +T. U. Muenchen<br>
   2.152  D-80290 Muenchen<br>
   2.153  Germany<br>
   2.154  <br>