# HG changeset patch # User wenzelm # Date 957558207 -7200 # Node ID 85539b33be03910346fe533878c4f89e31654629 # Parent 204f4ebbba6419ba5c6d43df47737edbec344015 updated; diff -r 204f4ebbba64 -r 85539b33be03 INSTALL --- 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$ diff -r 204f4ebbba64 -r 85539b33be03 README.html --- 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 @@ - @@ -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.

@@ -43,38 +42,38 @@ The following ML system and platform combinations are known to work very well:

-

Poly/ML, 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. +

Poly/ML, 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.

SML/NJ -needs lots of store and disk space, but it is free. The current -official release is 110 (there is an RPM -archive 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. -

MLWorks is a commercial ML programming environment developed by -Harlequin 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. - +

MLWorks is a commercial ML programming environment developed by Harlequin 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.

Installation

-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 INSTALL 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 INSTALL as +distributed with Isabelle for more information. + Further background information may be found in the Isabelle System Manual, distributed with the sources (directory doc). @@ -82,33 +81,51 @@

User interfaces

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: - +

Other sources of information

+

The Isabelle Page

+ +The Isabelle home page may be accessed both from Cambridge and Munich: + + + +

Mailing list

-The electronic mailing list isabelle-users@cl.cam.ac.uk +The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems and exchange -information. To join, send a message to -isabelle-users-request@cl.cam.ac.uk. +information. To join, send a message to isabelle-users-request@cl.cam.ac.uk.

Personal mail

@@ -130,7 +147,7 @@ Tobias Nipkow
Institut fuer Informatik
-T. U. Muenchen
+T. U. Muenchen
D-80290 Muenchen
Germany