1.1 --- a/README Thu Nov 14 16:01:36 1996 +0100
1.2 +++ b/README Mon Nov 18 16:26:08 1996 +0100
1.3 @@ -15,15 +15,53 @@
1.4 separately using the Makefiles in the respective directories; read them for
1.5 more information.
1.6
1.7 - THE MAKEFILES
1.8 + HOW TO BUILD ISABELLE
1.9
1.10 -The Makefiles can use two different Standard ML compilers: Poly/ML version
1.11 -2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
1.12 -(Version 0.93 or later). Poly/ML is a commercial product and costs money,
1.13 -but it is reliable and its database system is convenient for interactive
1.14 -work. SML of New Jersey requires lots of store and disc space, but it is
1.15 -free and its code sometimes runs faster. Both compilers are perfectly
1.16 -satisfactory for running Isabelle.
1.17 +Here are brief instructions. For more detail, read further.
1.18 +
1.19 +1. Create a directory to hold the Isabelle executable images, and
1.20 + set the environment variable ISABELLEBIN to its pathname.
1.21 +
1.22 +2. Set the environment variable ISABELLECOMP to the command to execute your
1.23 + Standard ML compiler.
1.24 +
1.25 +3. If using Poly/ML, set the environment variable ML_DBASE to the pathname
1.26 + of the empty Poly/ML database.
1.27 +
1.28 +4. Change your working directory to that containing this file.
1.29 +
1.30 +5a. To build ALL logics and run examples, type "make-all" and wait up to
1.31 + 10 hours. Standard ML of New Jersey will require up to 200M
1.32 + of disc space! Poly/ML will require about 25M.
1.33 +
1.34 +-OR-
1.35 +5b. To build ALL logics but run no examples, type "make-all -notest". This
1.36 + is much faster than 5a but needs just as much disc space.
1.37 +
1.38 +-OR-
1.39 +5c. To build just one logic, such as HOL, change to directory HOL and type
1.40 + "make" or "make test". This may trigger further Makes automatically.
1.41 +
1.42 +
1.43 + SUITABLE ML COMPILERS
1.44 +
1.45 +You use two different Standard ML compilers: Poly/ML version 2.03 or later
1.46 +(from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or
1.47 +later). Poly/ML is a commercial product and costs money, but it is stable and
1.48 +efficient; moreover its database system is convenient for interactive work.
1.49 +SML of New Jersey requires lots of store and disc space, but it is free and
1.50 +its code sometimes runs faster. Both compilers are perfectly satisfactory for
1.51 +running Isabelle.
1.52 +
1.53 +To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel
1.54 +University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk.
1.55 +
1.56 +To obtain Standard ML of New Jersey, see the Web page
1.57 + http://cm.bell-labs.com/cm/cs/what/smlnj/software.html
1.58 +or send email to sml-nj@research.bell-labs.com.
1.59 +
1.60 +
1.61 + ENVIRONMENT VARIABLES
1.62
1.63 The Makefiles and make-all use environment variables that you should set
1.64 according to your site configuration. See file Tools/make-all-nj for an
1.65 @@ -37,16 +75,15 @@
1.66 ML_DBASE is an *absolute* pathname to the initial Poly/ML database. It is not
1.67 required for New Jersey ML.
1.68
1.69 -ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "/bin/sml".
1.70 +ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly
1.71 +-noDisplay -h 15000". (The -h switch to Poly specifies an initial heap
1.72 +allocation, which you should consider increasing if a command fails with the
1.73 +message "Run out of store".)
1.74 +
1.75 If, after stripping a leading pathname, the compiler begins with the letters
1.76 "poly" then the Makefiles assume Poly/ML. If it begins with the letters "sml"
1.77 then they assume Standard ML of New Jersey.
1.78
1.79 -If a Poly/ML session fails with the message "Run out of store" then you
1.80 -have used up the entire heap. If your tactic is not in a loop, allocating
1.81 -more heap at startup should correct the problem. For instance, "poly -h
1.82 -15000" allocates sufficient heap space to rebuild all Isabelle examples.
1.83 -
1.84
1.85 STRUCTURE OF THIS DIRECTORY
1.86
1.87 @@ -57,17 +94,19 @@
1.88 Tools contains shell scripts and utilities
1.89
1.90 The following subdirectories contain object-logics:
1.91 - FOL Natural deduction First-Order Logic (intuitionistic and classical)
1.92 - FOLP First-Order Logic with Proof terms
1.93 - ZF Zermelo-Fraenkel set theory
1.94 - HOL Classical Higher-Order Logic
1.95 - LCF Logic for Computable Functions (domain theory) built upon FOL
1.96 - HOLCF A version of LCF built upon HOL
1.97 - CTT Constructive Type Theory
1.98 - LK Classical first-order sequent calculus
1.99 - Modal The modal logics T, S4, S43
1.100 - CCL Martin Coen's Classical Computational Logic
1.101 - Cube Barendregt's Lambda Cube
1.102 + FOL natural deduction First-Order Logic
1.103 + (intuitionistic and classical versions)
1.104 + FOLP First-Order Logic with Proof terms
1.105 + ZF Zermelo-Fraenkel set theory
1.106 + HOL Classical Higher-Order Logic
1.107 + LCF Logic for Computable Functions (domain theory) built upon FOL
1.108 + HOLCF A version of LCF built upon HOL
1.109 + CTT Constructive Type Theory
1.110 + Sequents Sequent calcul: first-order logic
1.111 + modal logics T, S4, S43
1.112 + intuitionistic linear logic
1.113 + CCL Martin Coen's Classical Computational Logic
1.114 + Cube Barendregt's Lambda Cube
1.115
1.116 David Aspinall has written a user interface for Isabelle. It runs under
1.117 GNU Emacs. It's useful to both novices and experts. You can get it by ftp
1.118 @@ -79,23 +118,11 @@
1.119 good way to get started.
1.120
1.121 Each object-logic is built on top of Pure Isabelle, and possibly on top of
1.122 -another object logic like FOL or LK. A database or binary called Pure is
1.123 +another object logic like FOL or HOL. A database or binary called Pure is
1.124 first created, then the object-logic is loaded on top. Poly/ML extends
1.125 Pure using its "make_database" operation. Standard ML of New Jersey starts
1.126 with the Pure core image and loads the object-logic's ROOT.ML.
1.127
1.128 - HOW TO GET A STANDARD ML COMPILER
1.129 -
1.130 -To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract
1.131 -Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
1.132 -England.
1.133 -
1.134 -To obtain Standard ML of New Jersey, contact David MacQueen
1.135 -<dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,
1.136 -Murray Hill, NJ 07974, USA. This compiler is available by FTP. Connect to
1.137 -research.att.com; login as anonymous with your userid as password; set
1.138 -binary mode; transfer files from the directory dist/ml.
1.139 -
1.140 ------------------------------------------------------------------------------
1.141
1.142 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum