README
changeset 2189 c00533aec02f
parent 2119 1d8ae796f3bf
child 2213 a96a7b6c0437
     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 +Here are brief instructions.  For more detail, read further.
    1.11 +
    1.12 +1.  Create a directory to hold the Isabelle executable images, and 
    1.13 +    set the environment variable ISABELLEBIN to its pathname.
    1.14 +
    1.15 +2.  Set the environment variable ISABELLECOMP to the command to execute your
    1.16 +    Standard ML compiler.
    1.17 +
    1.18 +3.  If using Poly/ML, set the environment variable ML_DBASE to the pathname
    1.19 +    of the empty Poly/ML database.
    1.20 +
    1.21 +4.  Change your working directory to that containing this file.
    1.22 +
    1.23 +5a. To build ALL logics and run examples, type "make-all" and wait up to 
    1.24 +    10 hours.  Standard ML of New Jersey will require up to 200M
    1.25 +    of disc space!  Poly/ML will require about 25M.
    1.26 +
    1.27 +-OR-
    1.28 +5b. To build ALL logics but run no examples, type "make-all -notest".  This
    1.29 +    is much faster than 5a but needs just as much disc space.
    1.30  
    1.31 -The Makefiles can use two different Standard ML compilers: Poly/ML version
    1.32 -2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
    1.33 -(Version 0.93 or later).  Poly/ML is a commercial product and costs money,
    1.34 -but it is reliable and its database system is convenient for interactive
    1.35 -work.  SML of New Jersey requires lots of store and disc space, but it is
    1.36 -free and its code sometimes runs faster.  Both compilers are perfectly
    1.37 -satisfactory for running Isabelle.
    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