Installation of Isabelle-2005 with Poly/ML-5.2.1 and ProofGeneral-3.7.1

Isabelle-2005 has to be slightly modified to run with up-to-date versions of Poly/ML and ProofGeneral.

  • Download the patch, which contains the following changes necessary to run Isabelle-2005 with Poly/ML-5.2.1 and ProofGeneral-3.7.1:
    • Updated the Poly/ML runtime system version detection script lib/scripts/polyml-version to the version from the Isabelle-2008 distribution.
    • Updated the Poly/ML platform detection script lib/scripts/polyml-platform to the version from the Isabelle-2008 distribution.
    • Added Poly/ML 5.2 startup script lib/scripts/run-polyml-5.2 from the Isabelle-2008 distribution (known there as lib/scripts/run-polyml).
    • Added Poly/ML 5.2 compability file src/Pure/ML-Systems/polyml-5.2.ML thankfully provided by Makarius Wenzel.
    • Adapted etc/settings to ProofGeneral 3.7, patch by Makarius Wenzel, see http://isabelle.in.tum.de/repos/isabelle/rev/9053fd546501.
    • Added wrappers for Poly/ML 5.2.1.

  • Extract the Isabelle archive and apply the patch. Assuming a GNU/Linux environment and assuming that both patch and tar files are in the same directory, the following commands can be used:
    tar xzf Isabelle2005.tar.gz
    cd Isabelle2005
    patch -p1 < ../Isabelle-2005_PolyML-5.2.1_ProofGeneral-3.7.1.patch
    chmod 755 lib/scripts/run-polyml-5.2
    chmod 755 lib/scripts/run-polyml-5.2.1

  • The rest of the installation procedure is standard (i.e., install Poly/ML-5.2.1 and ProofGeneral-3.7.1 where Isabelle can find it and build necessary heaps, e.g., HOL).

  • Please note that starting from version 3.7, ProofGeneral defaults to using emacs, not XEmacs, so an additional option -p xemacs given on start-up or put in PROOFGENERAL_OPTIONS in the Isabelle settings file etc/settings may be required to run ProofGeneral with an XEmacs front-end. (Similarly, rebuilding ProofGeneral for XEmacs may be required, see the installation notes in the ProofGeneral distribution.)

  • Please contact if you experience problems or want to provide feedback.

 
Revision 01 Jan 2009