Interactive Theorem Proving live!

ITP live! is a live CD with a bunch of interactive theorem prover installed. It is based on the Debian GNU/Linux distribution and is prepared using the Live helper utility.

Written by Enrico Tassi.

Current content

The following provers are included:

Coq 8.1, Why 2.02, Krakatoa 0.68
Mizar 7.8.05/4.84.971
Isabelle 07-May-2007
Epigram1 11 Oct 2006
Agda 2.1.0
Matita svn snapshot

The following software is also available in the CD:

Gnome desktop environment
Epiphany web browser and Evolution mail/calendar suite
Vim and Emacs/XEmacs
Proof General
svn, cvs, ssh, rdesktop, hibernate

Download ISO

You can download the following image(s).

binary.iso
md5: a4ec0a90437030f347d1229678b47dd6
size: 598M

Requisites to run the CD

To boot from the CD/USB you need the following hardware:

i486 compatible hardware (note that amd64 and Core 2 are also fine)
256M of ram (may work with less, but is untested)

You may also run the CD/USB within an emulator, like qemu or virtualbox, if you have a different architecture (like powerpc) or you don't want to reboot your computer, or the livecd fails to boot cause you have some exotic hardware supported only by proprietary drivers (yes, qemu/virtualbox run on Windows and MacOS X too).

Known bugs/Feature requests

Please report any bug you find to the author (Enrico Tassi)

geyser3 touch-pad (MacBook2.1) is not recognised resulting in only one mouse button (no synaptic, no two finger tapping support)
missing icons for Epigram
Xemacs terminal emulation not supporting colors

ChangeLog

Mon Sep 10 12:24:10 BST 2007

Added samba client
Added file-roller
Added all slides/exercises of the Types Summer School 07

Thu Sep 6 15:17:22 BST 2007

Modular homepage
Both iso and usb images are now produced

Fri Aug 17 12:58:18 BST 2007

Updated Mizar
Added Nipkow and Wenzel stuff

Tue Jul 24 15:38:54 BST 2007

Krakatoa 0.68

Mon Jul 23 16:32:11 BST 2007

More doc for Isabelle
New version of Matita
Fixed some emacs issues

Thu Jul 19 16:53:29 BST 2007

Added Simplify, ergo and yices
Added some utils to make wifi network work

Wed Jul 18 13:58:38 BST 2007

Agda 2.1.0 seems ready

Mon Jul 9 13:47:06 BST 2007

Tentative addition of Agda 2.0.1

Wed Jul 4 21:50:35 BST 2007

Added evince
Removed gcc that was pulled in by linux-wlan-ng-firmware
New proofgeneral snapshot
New default file for Isabelle Scratch.thy
Fixed matita example file
Only few pdf files are linked insidethe isabelle documentation dir

Tue Jul 3 18:39:48 BST 2007

Added persistence and some notes about it in the help file
Changed grub splash image, new ITP live/Debian theme
Added a mail client and a web browser
Added gnome-volume-manager

Tue May 22 10:02:06 CEST 2007

Added Matita (an svn snapshot)
Moved from gnome to gnome-core to free some space

Mon May 14 10:27:53 CEST 2007

Installed Proof-General snapshot in /usr/local/ for Isabelle
Fixed isabelle.setting file according to Macarius suggestions
Removed Isabelle spurious documentation and added symlinks in /usr/local/bin/ to isabelle and isatool
Added pommed and 915resolution packages for Intel MacBook