Admin/Isabelle2005-polyml-5.0/README-polyml-5.0
author wenzelm
Fri Dec 29 17:24:46 2006 +0100 (2006-12-29)
changeset 21935 4e20a5397b57
parent 21764 720b0add5206
permissions -rw-r--r--
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
     1 
     2 Using Isabelle2005 with Poly/ML 5.0 requires the following
     3 compatibility wrappers:
     4 
     5   Isabelle2005/src/Pure/ML-Systems/polyml-5.0.ML
     6   Isabelle2005/lib/scripts/run-polyml-5.0
     7 
     8 The Isabelle settings need to specify that version, by including
     9 something like this in Isabelle2005/etc/settings or
    10 ~/isabelle/etc/settings:
    11 
    12   ML_PLATFORM=""
    13   ML_HOME=/usr/local/bin
    14   ML_SYSTEM=polyml-5.0
    15   ML_OPTIONS="-H 500"
    16 
    17 Now logics can be compiled as usual, cf. the INSTALL instructions.
    18 
    19 
    20 ProofGeneral needs to be adapted as well, by including the following
    21 in Isabelle2005/etc/proofgeneral-settings.el or
    22 ~/isabelle/etc/proofgeneral-settings.el:
    23 
    24   (custom-set-variables
    25    '(proof-shell-pre-interrupt-hook (lambda () t)))
    26 
    27 Otherwise ProofGeneral will regard polyml-5.0 as an old polyml-3.x and
    28 activate strange workarounds for interrupt handling.
    29 
    30 
    31 	Makarius
    32 	11-Dec-2006
    33 
    34 $Id$