Ich habe (inoffizielle) Debian Pakete für Isabelle 2008 und den dafür benötigten Programmen erstellt. Dies sind unter anderem:
sowie
Binärpakete kann ich leider nur für die i386 Architektur von GNU/Linux anbieten. Die Quellpakete sollten aber auf jeder Architektur, die von Poly/ML unterstützt wird, verwendbar sein.
Die Installation von Isabelle 2008 (und HOL-TestGen) auf einem Debian GNU/Linux sollte unkompliziert sein. Es muss lediglich das IsaMorph Repository als apt-Quelle beim Paketmanager eingetragen werden; zum Beispiel durch Eintragen von folgenden Zeilen in die Datei /etc/apt/sources.list:
# IsaMorph repository (https://www.brucker.ch/projects/debian/) deb http://projects.brucker.ch/debian/rep stable main non-free deb-src http://projects.brucker.ch/debian/rep stable main non-free
# IsaMorph repository (https://www.brucker.ch/projects/debian/) deb http://projects.brucker.ch/debian/rep testing main non-free deb-src http://projects.brucker.ch/debian/rep testing main non-free
# IsaMorph repository (https://www.brucker.ch/projects/debian/) deb http://projects.brucker.ch/debian/rep unstable main non-free deb-src http://projects.brucker.ch/debian/rep unstable main non-free
Jetzt muss die Paket-Datenbank aktualisiert werden:
aptitude update
Isabelle kann nun installiert werden durch folgenden Befehl:
aptitude install polyml proofgeneral-misc isabelle isabelle-thy-hol
Dies sollte zu eine lauffähigen Installation von SML/NJ, Isabelle, und Proof General führen. Die verschiedenen Logiken stehen als isabelle-thy-hol-NAME zur Verfügung (NAME steht hierbei für die zu installierende Logik), z.B. isabelle-thy-zf oder isabelle-thy-hol-complex). Zusätzlich kann HOL-TestGen durch folgenden Befehl installiert werden:
aptitude install hol-testgen hol-testgen-doc
Für die meisten Pakete ist die Dokumentation als seperates -doc Paket (z.B. isabelle-doc) verfügbar. In den meisten Fällen ist es ratsam, diese auch zu installieren.
Jetzt sollte es möglich sein, Isabelle (oder hol-testgen) auf der Kommandozeile zu starten. Zudem sollten es im Bereich Mathematik entsprechende Einträge im Menüsystem der Benutzeroberfläche geben.
Während den Arbeiten zu IsaMorph habe ich (inoffizielle) Debian Pakete für Isabelle 2005 und den dafür benötigten Programmen erstellt. Dies sind unter anderem:
sowie
Binärpakete kann ich leider nur für die i386 Architektur von GNU/Linux anbieten. Die Quellpakete sollten aber auf jeder Architektur, die von SML unterstützt wird, verwendbar sein.
Die Installation von Isabelle 2005 (und HOL-TestGen) auf einem Debian GNU/Linux sollte unkompliziert sein. Es muss lediglich das IsaMorph Repository als apt-Quelle beim Paketmanager eingetragen werden; zum Beispiel durch Eintragen von folgenden Zeilen in die Datei /etc/apt/sources.list:
deb http://kisogawa.inf.ethz.ch/isamorph/debian stable main deb-src http://kisogawa.inf.ethz.ch/isamorph/debian stable main
deb http://kisogawa.inf.ethz.ch/isamorph/debian testing main deb-src http://kisogawa.inf.ethz.ch/isamorph/debian testing main
deb http://kisogawa.inf.ethz.ch/isamorph/debian unstable main deb-src http://kisogawa.inf.ethz.ch/isamorph/debian unstable main
Jetzt muss die Paket-Datenbank aktualisiert werden:
aptitude update
Isabelle kann nun installiert werden durch folgenden Befehl:
aptitude install x-symbol proofgeneral-misc isabelle isabelle-thy-hol
Dies sollte zu eine lauffähigen Installation von SML/NJ, Isabelle, und Proof General führen. Die verschiedenen Logiken stehen als isabelle-thy-hol-NAME zur Verfügung (NAME steht hierbei für die zu installierende Logik), z.B. isabelle-thy-zf oder isabelle-thy-hol-complex). Zusätzlich kann HOL-TestGen durch folgenden Befehl installiert werden:
aptitude install hol-testgen hol-testgen-doc
Für die meisten Pakete ist die Dokumentation als seperates -doc Paket (z.B. isabelle-doc) verfügbar. In den meisten Fällen ist es ratsam, diese auch zu installieren.
Jetzt sollte es möglich sein, Isabelle (oder hol-testgen) auf der Kommandozeile zu starten. Zudem sollten es im Bereich Mathematik entsprechende Einträge im Menüsystem der Benutzeroberfläche geben.