Unofficial Debian Repository for Isabelle 2008 and related stuff

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 Using the Debian Package Manager

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:

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.

Unofficial Debian Repository for Isabelle 2005 and related stuff

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 Using the Debian Package Manager

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:

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.