Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/Isabelle2005-polyml-5.0/README-polyml-5.0
author aspinall
Mon, 22 Jan 2007 16:53:33 +0100
changeset 22165 eaec72532dd7
parent 21764 720b0add5206
permissions -rw-r--r--
Add location_of_position. Needs work elsewhere.


Using Isabelle2005 with Poly/ML 5.0 requires the following
compatibility wrappers:

  Isabelle2005/src/Pure/ML-Systems/polyml-5.0.ML
  Isabelle2005/lib/scripts/run-polyml-5.0

The Isabelle settings need to specify that version, by including
something like this in Isabelle2005/etc/settings or
~/isabelle/etc/settings:

  ML_PLATFORM=""
  ML_HOME=/usr/local/bin
  ML_SYSTEM=polyml-5.0
  ML_OPTIONS="-H 500"

Now logics can be compiled as usual, cf. the INSTALL instructions.


ProofGeneral needs to be adapted as well, by including the following
in Isabelle2005/etc/proofgeneral-settings.el or
~/isabelle/etc/proofgeneral-settings.el:

  (custom-set-variables
   '(proof-shell-pre-interrupt-hook (lambda () t)))

Otherwise ProofGeneral will regard polyml-5.0 as an old polyml-3.x and
activate strange workarounds for interrupt handling.


	Makarius
	11-Dec-2006

$Id$
isabelle