Updated instructions
authorpaulson
Wed Nov 27 13:04:04 1996 +0100 (1996-11-27)
changeset 22492af17dd5479e
parent 2248 187d001fbe79
child 2250 891eb76b8045
Updated instructions
README
     1.1 --- a/README	Wed Nov 27 13:01:07 1996 +0100
     1.2 +++ b/README	Wed Nov 27 13:04:04 1996 +0100
     1.3 @@ -19,14 +19,14 @@
     1.4  
     1.5  Here are brief instructions.  For more detail, read further.
     1.6  
     1.7 -1.  Create a directory to hold the Isabelle executable images, and 
     1.8 -    set the environment variable ISABELLEBIN to its pathname.
     1.9 +1.  Create a directory to hold the Isabelle executable images.
    1.10 +    Set the environment variable ISABELLEBIN to its full (absolute) pathname.
    1.11  
    1.12  2.  Set the environment variable ISABELLECOMP to the command to execute your
    1.13      Standard ML compiler.
    1.14  
    1.15 -3.  If using Poly/ML, set the environment variable ML_DBASE to the pathname
    1.16 -    of the empty Poly/ML database.
    1.17 +3.  If using Poly/ML, set the environment variable ML_DBASE to the full 
    1.18 +    pathname of the empty Poly/ML database.
    1.19  
    1.20  4.  Change your working directory to that containing this file.
    1.21  
    1.22 @@ -49,10 +49,10 @@
    1.23  (from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or
    1.24  later).  Poly/ML is a commercial product and costs money, but it is stable and
    1.25  efficient; moreover its database system is convenient for interactive work.
    1.26 -SML/NJ needs lots of store and disc space, but it is free.  Recent versions of
    1.27 -SML/NJ are significantly faster than 0.93, but beware of many
    1.28 +SML/NJ needs lots of store and disc space, but it is free.  Some recent
    1.29 +versions of SML/NJ are significantly faster than 0.93, but beware of many
    1.30  incompatibilities among them; you might be forced to edit the file
    1.31 -Pure/NJ1xx.ML.
    1.32 +Pure/NJ1xx.ML.  VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW.
    1.33  
    1.34  To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel
    1.35  University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk.
    1.36 @@ -70,8 +70,7 @@
    1.37  
    1.38  ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    1.39  images.  This directory *must* be different from the Isabelle source
    1.40 -directory.  When using Poly/ML, ISABELLEBIN must be an absolute pathname
    1.41 -(one starting with "/").
    1.42 +directory.  ISABELLEBIN must be an absolute pathname (one starting with "/").
    1.43  
    1.44  ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
    1.45  required for New Jersey ML.
    1.46 @@ -79,7 +78,9 @@
    1.47  ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly
    1.48  -noDisplay -h 15000".  (The -h switch to Poly specifies an initial heap
    1.49  allocation, which you should consider increasing if a command fails with the
    1.50 -message "Run out of store".)
    1.51 +message "Run out of store".)  Please DO NOT use a command such as
    1.52 +"sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the
    1.53 +Makefiles. 
    1.54  
    1.55  If, after stripping a leading pathname, the compiler begins with the letters
    1.56  "poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"