README
changeset 2249 2af17dd5479e
parent 2213 a96a7b6c0437
equal deleted inserted replaced
2248:187d001fbe79 2249:2af17dd5479e
    17 
    17 
    18 			HOW TO BUILD ISABELLE
    18 			HOW TO BUILD ISABELLE
    19 
    19 
    20 Here are brief instructions.  For more detail, read further.
    20 Here are brief instructions.  For more detail, read further.
    21 
    21 
    22 1.  Create a directory to hold the Isabelle executable images, and 
    22 1.  Create a directory to hold the Isabelle executable images.
    23     set the environment variable ISABELLEBIN to its pathname.
    23     Set the environment variable ISABELLEBIN to its full (absolute) pathname.
    24 
    24 
    25 2.  Set the environment variable ISABELLECOMP to the command to execute your
    25 2.  Set the environment variable ISABELLECOMP to the command to execute your
    26     Standard ML compiler.
    26     Standard ML compiler.
    27 
    27 
    28 3.  If using Poly/ML, set the environment variable ML_DBASE to the pathname
    28 3.  If using Poly/ML, set the environment variable ML_DBASE to the full 
    29     of the empty Poly/ML database.
    29     pathname of the empty Poly/ML database.
    30 
    30 
    31 4.  Change your working directory to that containing this file.
    31 4.  Change your working directory to that containing this file.
    32 
    32 
    33 5a. To build ALL logics and run examples, type "make-all" and wait up to 
    33 5a. To build ALL logics and run examples, type "make-all" and wait up to 
    34     10 hours.  Standard ML of New Jersey will require up to 200M
    34     10 hours.  Standard ML of New Jersey will require up to 200M
    47 
    47 
    48 You can use two different Standard ML compilers: Poly/ML version 2.03 or later
    48 You can use two different Standard ML compilers: Poly/ML version 2.03 or later
    49 (from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or
    49 (from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or
    50 later).  Poly/ML is a commercial product and costs money, but it is stable and
    50 later).  Poly/ML is a commercial product and costs money, but it is stable and
    51 efficient; moreover its database system is convenient for interactive work.
    51 efficient; moreover its database system is convenient for interactive work.
    52 SML/NJ needs lots of store and disc space, but it is free.  Recent versions of
    52 SML/NJ needs lots of store and disc space, but it is free.  Some recent
    53 SML/NJ are significantly faster than 0.93, but beware of many
    53 versions of SML/NJ are significantly faster than 0.93, but beware of many
    54 incompatibilities among them; you might be forced to edit the file
    54 incompatibilities among them; you might be forced to edit the file
    55 Pure/NJ1xx.ML.
    55 Pure/NJ1xx.ML.  VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW.
    56 
    56 
    57 To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel
    57 To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel
    58 University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk.
    58 University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk.
    59 
    59 
    60 To obtain Standard ML of New Jersey, see the Web page 
    60 To obtain Standard ML of New Jersey, see the Web page 
    68 according to your site configuration.  See file Tools/make-all-nj for an
    68 according to your site configuration.  See file Tools/make-all-nj for an
    69 example using the Bourne shell, sh.
    69 example using the Bourne shell, sh.
    70 
    70 
    71 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    71 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    72 images.  This directory *must* be different from the Isabelle source
    72 images.  This directory *must* be different from the Isabelle source
    73 directory.  When using Poly/ML, ISABELLEBIN must be an absolute pathname
    73 directory.  ISABELLEBIN must be an absolute pathname (one starting with "/").
    74 (one starting with "/").
       
    75 
    74 
    76 ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
    75 ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
    77 required for New Jersey ML.
    76 required for New Jersey ML.
    78 
    77 
    79 ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly
    78 ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly
    80 -noDisplay -h 15000".  (The -h switch to Poly specifies an initial heap
    79 -noDisplay -h 15000".  (The -h switch to Poly specifies an initial heap
    81 allocation, which you should consider increasing if a command fails with the
    80 allocation, which you should consider increasing if a command fails with the
    82 message "Run out of store".)
    81 message "Run out of store".)  Please DO NOT use a command such as
       
    82 "sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the
       
    83 Makefiles. 
    83 
    84 
    84 If, after stripping a leading pathname, the compiler begins with the letters
    85 If, after stripping a leading pathname, the compiler begins with the letters
    85 "poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
    86 "poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
    86 then they assume Standard ML of New Jersey.
    87 then they assume Standard ML of New Jersey.
    87 
    88