--- a/INSTALL Fri May 05 22:18:40 2000 +0200
+++ b/INSTALL Fri May 05 22:23:27 2000 +0200
@@ -1,67 +1,148 @@
-Isabelle compilation and installation notes
+Isabelle installation and compilation notes
===========================================
-Unpacking the archive
----------------------
+1) User installation
+--------------------
+
+Here we assume that Isabelle has already been installed at your site.
+Otherwise see 2) below of how to get the Isabelle system installed in
+the first place.
+
+
+1a) Running the Isabelle binaries
+---------------------------------
+
+The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
+directly from their location within the distribution directory
+[ISABELLE_HOME] like this:
+
+ [ISABELLE_HOME]/bin/isabelle HOL
+
+This starts an interactive Isabelle session within your current text
+terminal. You may want to put [ISABELLE_HOME]/bin into your shell's
+search PATH, but this is not strictly necessary.
+
+
+Please do *not* copy (or link) the Isabelle scripts anywhere else ---
+they just won't work! If you really want to install independent
+Isabelle binaries somewhere else then do it like this:
+
+ [ISABELLE_HOME]/bin/isatool install -p ~/bin
-After unpacking the Isabelle distribution archive (using tar and gzip)
-you are left with some directory IsabelleYY-X. You may install this
-anywhere, but please just *not* as ~/isabelle!!!
+Your site-wide Isabelle installation may already provide Isabelle
+executables in some global bin directory (such as /usr/bin).
+
+
+1b) Isabelle as KDE application
+-------------------------------
+
+Isabelle may be installed as application icon on the KDE desktop like
+this:
+
+ [ISABELLE_HOME]/bin/isatool install -k
-The place where you put the contents of IsabelleYY-X will be referred
-to as [ISABELLE_HOME] subsequently.
+Clicking on that icon will invoke the interface wrapper script
+(capital Isabelle), which may be configured to run your favorite
+Isabelle user interface via the ISABELLE_INTERFACE setting.
+Additional options may be passed by editing the application's command
+line (by using the standard KDE desktop functionality).
+
+
+2) System installation
+----------------------
+
+The Isabelle distribution is available both as traditional source-only
+tar.gz archives, and as binary packages (currently only RPM for
+Linux/x86). In any case, the resulting Isabelle installation always
+contains the full sources, thus any part of the system be recompiled
+later, too.
-Auto configuration
+2a) Binary installation
+----------------------
+
+Ready-to-go RPM packages are provided for the ML compiler and runtime
+system, the Isabelle sources, and some major object-logics. These
+packages should work on any major RPM-based Linux/x86 platform (such
+as SuSE, RedHat etc.). A typical installation procedure would be like
+this (executed as root):
+
+ rpm -i smlnj-110.0-3.i386.rpm
+ rpm -i --prefix /usr/share isabelle.rpm
+ rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
+
+The install prefix may be changed as indicated. By default the ML
+system is expected to be at the same directory level as Isabelle
+itself; changing this arrangement requires
+[ISABELLE_HOME]/etc/settings to be adapted manually.
+
+
+Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
+Isabelle as platform independent sources. Precompiled object-logics
+are provided for convenience.
+
+
+Recompiling logics
------------------
-There are some minor adaptions to be made of the Isabelle distribution
-to your system environment. Simply type:
+Some people prefer to be able to reconstruct the full system from the
+sources, rather than installing RPM packages blindly. We do not
+provide source RPMs, yet any parts of Isabelle may be recompiled after
+installation of the main isabelle.rpm package (which contains only
+sources anyway).
+
+Assuming proper configuration of the underlying ML system, Isabelle
+object-logics may be recompiled like this:
+
+ [ISABELLE_HOME]/build HOL FOL
+
+
+Source installation
+-------------------
+
+Traditional tar.gz archives are provided for the full Isabelle sources
+and documentation as well. Make sure your ML system (SML/NJ, Poly/ML
+etc.) has already been installed properly; then proceed as follows.
+
+
+* Unpacking the archives. After unpacking the Isabelle distribution
+archives (using tar and gzip) you are left with some directory
+IsabelleYY-X. Basically, this may be installed anywhere --- just note
+that ~/isabelle would be a really bad idea, though. The place where
+you put the contents of IsabelleYY-X will be referred to as
+[ISABELLE_HOME] subsequently.
+
+
+* Auto configuration. There are some minor adaptions to be made of
+the Isabelle distribution to your system environment (mostly locations
+of bash and perl). Simply do it like this:
cd [ISABELLE_HOME]
./configure
-This does not store any references to [ISABELLE_HOME]. You may safely
-move the system later, without running ./configure again.
+Note that this does not store any references to [ISABELLE_HOME]. You
+may safely move the system later, without having to run ./configure
+again.
-ML system settings and compilation
-----------------------------------
-
-Before actual compilation you have to tell Isabelle about your
-Standard ML system. These settings reside in ./etc/settings, which
-may be also overridden by ~/isabelle/etc/settings. There are already
-various sample configurations in ./etc/settings commented out.
+* ML system settings and compilation. Before actual compilation you
+have to tell Isabelle about your Standard ML system. These settings
+reside in ./etc/settings, which may be also overridden by
+~/isabelle/etc/settings. There are already various sample
+configurations in ./etc/settings commented out.
To build the core Isabelle/Pure and the default object-logic, just
-type:
+type
./build
-More object-logics can be made similarly:
+More object-logics can be made in a similar fashion:
./build FOL HOL
-
-Running the system
-------------------
-
-Provided that compilation was successful, you can now run something
-like:
-
- [ISABELLE_HOME]/bin/isabelle FOL
-
-This starts an interactive Isabelle session within your current text
-terminal. You may want to put [ISABELLE_HOME]/bin into your shell's
-search PATH.
-
-Please do *not* copy (or link) the Isabelle scripts anywhere else, or
-they just won't work! If you really feel the urge to install
-independent Isabelle binaries anywhere else do it like this:
-
- [ISABELLE_HOME]/bin/isatool install -p /usr/local/bin
-
+After successful compilation you are ready to run the system, see 1)
+above for more information.
$Id$
--- a/README.html Fri May 05 22:18:40 2000 +0200
+++ b/README.html Fri May 05 22:23:27 2000 +0200
@@ -1,4 +1,3 @@
-
<html>
<!-- $Id$ -->
@@ -25,7 +24,7 @@
starts at about 32-64 MB of free main memory (somewhat depending on
your ML system), with several tens of MB disk space and a decent CPU.
Speaking by today's hardware standards, any moderate Linux box should
-make a nice platform for Isabelle.
+give a very nice platform for Isabelle.
<p>
@@ -43,38 +42,38 @@
The following ML system and platform combinations are known to work
very well:
<ul>
-<li> Poly/ML 3.x on Linux and Suns.
-<li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns).
+<li> Poly/ML 3.x on Linux and Sparc/Solaris.
+<li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
<li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
problems with Linux and HP-UX, though.
</ul>
-<p> <A HREF="http://www.polyml.org/">Poly/ML</A>, previously a commercial
-product, is back in the public domain. It is the best compiler for running
-Isabelle, requiring the least memory and offering the fastest performance.
+<p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
+commercial product, is back in the free world. It is by far the best
+compiler for running Isabelle, requiring the least memory and offering
+the highest performance.
<p> <a
href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
-needs lots of store and disk space, but it is free. The current
-official release is 110 (there is an <a
-href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM
-archive</a> available for Linux/x86). We still support the old 0.93
-release, but do not recommend it.
+needs lots of store and disk space, but supports many more platforms.
+The current official release is 110. Basically, we still support the
+old 0.93 release, but do not recommend it.
-<p> MLWorks is a commercial ML programming environment developed by
-<a href="http://www.harlequin.com/">Harlequin</A> and was
-unfortunately withdrawn after that company was taken over. Isabelle on
-MLWorks 2.0 works well. It is about 20% faster than on SML/NJ while using
-slightly less memory and disk space. A few minor features (e.g. ML top-level
-pretty printing) are not supported, though.
-
+<p> MLWorks is a commercial ML programming environment developed by <a
+href="http://www.harlequin.com/">Harlequin</a> and was unfortunately
+withdrawn after that company was taken over. Isabelle on MLWorks 2.0
+works well. It is about 20% faster than on SML/NJ while using
+slightly less memory and disk space. A few minor features (e.g. ML
+top-level pretty printing) are not supported, though.
<h2>Installation</h2>
-Binary rpm packages are available for Isabelle/HOL and ZF on the
-Linux/x86 platform. Alternatively, the system may be built from
-scratch as described in file <tt>INSTALL</tt> of the Isabelle sources.
+RPM packages are available for Isabelle/HOL and ZF on the Linux/x86
+platform. The system may be easily built from scratch as well, taking
+the traditional tar.gz distribution. See file <tt>INSTALL</tt> as
+distributed with Isabelle for more information.
+
Further background information may be found in the <em>Isabelle System
Manual</em>, distributed with the sources (directory <tt>doc</tt>).
@@ -82,33 +81,51 @@
<h2>User interfaces</h2>
The distribution includes only a very primitive interface based on
-ordinary terminal sessions. Advanced interfaces are available from
+ordinary terminal sessions. Advanced interfaces are available from
other sources:
-<UL>
-<LI>
-<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
-David Aspinall is a more elaborate interface for Isabelle. It runs
-under recent versions of XEmacs and is useful to both novices and
-experts.
+<ul>
-<LI>
-<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> is
-a generic Emacs interface for proof assistants, including Isabelle
-(both for the classic and Isar version). Proof General is suitable
-for use by pacifists and Emacs militants alike. Its most prominent
-feature is script management, providing a metaphor of <em>live proof
-script editing</em>.
-</UL>
+<li>
+<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
+David Aspinall and others is a generic Emacs interface for proof
+assistants, including Isabelle (both for the classic and Isar
+version). Proof General is suitable for use by pacifists and Emacs
+militants alike. Its most prominent feature is script management,
+providing a metaphor of <em>live proof script editing</em>. Proof
+General has recently gained a rather large following of both beginning
+and expert users of Isabelle.
+
+<li>
+<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
+David Aspinall is an older and simpler Emacs interface for Isabelle.
+It runs under recent versions of XEmacs.
+
+</ul>
+
<h2>Other sources of information</h2>
+<h3>The Isabelle Page</h3>
+
+The Isabelle home page may be accessed both from Cambridge and Munich:
+
+<ul>
+
+<li> <a
+href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
+
+<li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
+
+</ul>
+
+
<h3>Mailing list</h3>
-The electronic mailing list <TT>isabelle-users@cl.cam.ac.uk</TT>
+The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
provides a forum for Isabelle users to discuss problems and exchange
-information. To join, send a message to
-<A HREF="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</A>.
+information. To join, send a message to <a
+href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.
<h3>Personal mail</h3>
@@ -130,7 +147,7 @@
<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
Institut fuer Informatik<br>
-T. U. Muenchen<br>
+T. U. Muenchen<br>
D-80290 Muenchen<br>
Germany<br>
<br>