README
changeset 2119 1d8ae796f3bf
parent 869 242b5050c1a6
child 2189 c00533aec02f
equal deleted inserted replaced
2118:7c12923a50c6 2119:1d8ae796f3bf
    35 (one starting with "/").
    35 (one starting with "/").
    36 
    36 
    37 ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
    37 ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
    38 required for New Jersey ML.
    38 required for New Jersey ML.
    39 
    39 
    40 ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml".  If
    40 ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "/bin/sml".
    41 ISABELLECOMP begins with the letters "poly" then the Makefiles assume that
    41 If, after stripping a leading pathname, the compiler begins with the letters
    42 it is Poly/ML; if it begins with the letters "sml" then they assume
    42 "poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
    43 Standard ML of New Jersey.  
    43 then they assume Standard ML of New Jersey.
    44 
    44 
    45 If a Poly/ML session fails with the message "Run out of store" then you
    45 If a Poly/ML session fails with the message "Run out of store" then you
    46 have used up the entire heap.  If your tactic is not in a loop, allocating
    46 have used up the entire heap.  If your tactic is not in a loop, allocating
    47 more heap at startup should correct the problem.  For instance, "poly -h
    47 more heap at startup should correct the problem.  For instance, "poly -h
    48 15000" allocates sufficient heap space to rebuild all Isabelle examples.
    48 15000" allocates sufficient heap space to rebuild all Isabelle examples.