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

 
Revision 28 Dec 2008