HOL-CASL: lokale Installation am CIP-Pool

HOL-CASL ist ein auf Isabelle/HOL basierendes, prototypisches Beweissystem für CASL-Spezifikationen und wird an der Uni Bremen entwickelt. Es ist am CIP-Pool unter Linux vorinstalliert, allerdings müssen einige Dateien im Homeverzeichnis des Benutzers angelegt werden, um mit HOL-CASL arbeiten zu können.

Kopieren Sie sich das hier zugängliche Archiv in Ihr Homeverzeichnis (als HOL-CASL.tgz) und entpacken Sie es mit den folgenden Befehlen:

    > cd
    > tar xfz HOL-CASL.tgz

(Das Archiv kann nach dem Entpacken gelöscht werden.) Sie erhalten ein Verzeichnis HOL-CASL mit einigen Unterverzeichnissen:

examples: enthält einige CASL-Beispiele. Ignorieren Sie Konstrukte, die in der Vorlesung nicht behandelt werden. Ihre eigenen CASL-Spezifikationen müssen ebenfalls in diesem Verzeichnis stehen, sonst können sie nicht geladen werden.
git: enthält einige Bibliotheken. Wichtig ist das Unterverzeichnis git/sessions/casl_win; dort werden die Sitzungsdateien abgespeichert. Die versteckte Datei git/sessions/casl_win/.last enthält den Namen der letzten Sitzung und dient zum Recovery.
sml_tk: enthält lediglich Bibliotheken.

Sie können das Archiv prinzipiell auch an einer beliebigen anderen Stelle unterhalb des Homeverzeichnis entpacken. Dann muss allerdings die Umgebungsvariable HOL_CASL auf das enstandene Unterverzeichnis zeigen (ihr Defaultwert ist $HOME/HOL-CASL).

Starten Sie HOL-CASL am besten aus einer Shell, damit Sie Fehlermeldungen usw. dort beobachten können.

Viel Erfolg beim Arbeiten! Bei Problemen schicken Sie bitte eine email an Stephan Merz.

Stephan Merz

Last modified: Tue Nov 7 10:23:35 CET 2000