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 Isabelle-2005 from the Isabelle release archive (direct link).

• 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.