I created (unofficial) Debian packages for Isabelle 2008 and its direct dependencies, e.g.:
and also
Note, I can only provide binary packages for GNU/Linux on a i386 architecture, but the source packages should built without problems on all architectures supported by Poly/ML.
Installing Isabelle 2008 (and also HOL-TestGen) on an Debian GNU/Linux should be straight forward. Just add the IsaMorph apt-repostory to the sources of your package manager, e.g., extend your /etc/apt/sources.list file by the following lines:
# 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
Now, update your package list, i.e., by executing
aptitude update
Now you can install Isabelle by executing
aptitude install polyml proofgeneral-misc isabelle isabelle-thy-hol
This should give you a running installation of Poly/ML, Isabelle, and Proof General. The different logics are packaged as isabelle-thy-hol-NAME, where NAME stands for the logic you want to install (e.g., isabelle-thy-zf or isabelle-thy-hol-complex). If you also want to install HOL-TestGen, just execute
aptitude install hol-testgen hol-testgen-doc
Note, most packages have also a documentation which is packaged seperately als -doc (e.g., isabelle-doc) package. In most cases you should also install these packages.
You should now be able to start Isabelle (or hol-testgen) from the command line. Further, you will also find entries in the menu system of your desktop environment (within the Math section). Happy proving.
While preparing IsaMorph I created (unofficial) Debian packages for Isabelle 2008 and its direct dependencies, e.g.:
and also
Note, I can only provide binary packages for GNU/Linux on a i386 architecture, but the source packages should built without problems on all architectures supported by SML.
Installing Isabelle 2005 (and also HOL-TestGen) on an Debian GNU/Linux should be straight forward. Just add the IsaMorph apt-repostory to the sources of your package manager, e.g., extend your /etc/apt/sources.list file by the following lines:
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
Now, update your package list, i.e., by executing
aptitude update
Now you can install Isabelle by executing
aptitude install x-symbol proofgeneral-misc isabelle isabelle-thy-hol
This should give you a running installation of SML/NJ, Isabelle, and Proof General. The different logics are packaged as isabelle-thy-hol-NAME, where NAME stands for the logic you want to install (e.g., isabelle-thy-zf or isabelle-thy-hol-complex). If you also want to install HOL-TestGen, just execute
aptitude install hol-testgen hol-testgen-doc
Note, most packages have also a documentation which is packaged seperately als -doc (e.g., isabelle-doc) package. In most cases you should also install these packages.
You should now be able to start Isabelle (or hol-testgen) from the command line. Further, you will also find entries in the menu system of your desktop environment (within the Math section). Happy proving.