Installation von Isabelle-2005 mit Poly/ML-5.2.1 und ProofGeneral-3.7.1

Isabelle-2005 muss leicht modifiziert werden, damit es zusammen mit aktuellen Versionen von Poly/ML und ProofGeneral läuft.

• Laden Sie Isabelle-2005 vom Isabelle Release Archiv herunter (direkter Link).

• Laden Sie den Patch herunter, der die notwendigen Änderungen an Isabelle-2005 für die Zusammenarbeit mit Poly/ML-5.2.1 und ProofGeneral-3.7.1 enthält:
  • Aktualisierung des Poly/ML Runtime System Versionserkennungsskripts lib/scripts/polyml-version gemäß der Version aus der Isabelle-2008 Distribution.
  • Aktualisierung des Poly/ML Plattformerkennungsskripts lib/scripts/polyml-platform gemäß der Version aus der Isabelle-2008 Distribution.
  • Hinzufügung eines Poly/ML 5.2 Startup Skripts lib/scripts/run-polyml-5.2 aus der Isabelle-2008 Distribution (heisst dort lib/scripts/run-polyml).
  • Hinzufügung der Poly/ML 5.2 Kompabilitätsdatei src/Pure/ML-Systems/polyml-5.2.ML, freundlicherweise von Makarius Wenzel bereitgestellt.
  • Anpassung von etc/settings für ProofGeneral 3.7, Patch von Makarius Wenzel, siehe http://isabelle.in.tum.de/repos/isabelle/rev/9053fd546501.
  • Bereitstellung von Wrappern für Poly/ML 5.2.1.

• Extrahieren Sie das Isabelle-Archiv und wenden Sie den Patch an. In einer GNU/Linux-Umgebung und unter der Annahme, dass Patch und Archiv im gleichen Verzeichnis liegen, können die folgenden Kommandos benutzt werden:
  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

• Die restliche Installationsprozedur läuft unverändert zur Standardinstallationsprozedur ab (d.h., Installation von Poly/ML-5.2.1 und ProofGeneral-3.7.1, so dass sie von Isabelle gefunden werden können, und Erstellung der erforderlichen Heaps, z.B. HOL).

• Bitte beachten Sie, dass ProofGeneral seit der Version 3.7 standardmäßig emacs, und nicht XEmacs, benutzt. Für die Benutzung von XEmacs ist also möglicherweise eine zusätzliche Option -p xemacs beim Start von Isabelle oder in PROOFGENERAL_OPTIONS in der Isabelle Konfigurationsdatei etc/settings erforderlich. (Ebenso muss ProofGeneral für XEmacs möglicherweise neu gebaut werden, siehe die Installationshinweise in der ProofGeneral Distribution.)

• Bitte wenden Sie sich bei Feedback oder Problemen an das .