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