Uni-Logo

Computer-Supported Modeling and Reasoning - Installation of Isabelle

Configuring your system for Isabelle

You will always run Isabelle by starting xemacs. For the first week's exercises, create a working directory and type xemacs ex1.ML. The file ex1.ML will be your first proof script, that is, a file containing Isabelle proofs. Now customize xemacs using the rich menus provided:
  • Multiple Windows: Isabelle will use several xemacs subwindows (simply windows in emacs jargon). You may choose if you want these displayed all in one window (called frame in emacs jargon) split into several parts or as several windows. This is done by (un)ticking the box "Proof-General:Options:Display:Multiple Windows".
  • X-Symbol: For a nice rendering of mathematical symbols, xemacs uses the X-symbol package. To enable it, tick the box "Proof-General:Options:X-Symbol".
  • Electric terminator: This will save you from having to type the return key to fire proof commands. Proceed in analogy to X-Symbol
  • Fly Past Comments: This will ignore comments when processing a proof step by step. Proceed in analogy to X-Symbol
  • Choosing the logic: We will use the logic FOL. Go to "Proof-General:Advanced:Customize:Isabelle:Chosen Logic". This will open a new buffer. Set the logic to "FOL" in this buffer and click "Save".
  • You should now select "Proof-General:Options:Save Options"

Installing Isabelle on your computer at home

Acknowledgement: Thanks to Achim Brucker for providing an accessible way of downloading Isabelle2005, and to Alexander Schimpf and Marcus Heizmann for their help in compiling these instructions.

If you want to use Isabelle on your computer (a linux system) at home, you should follow the instructions below. The following is a translation from Achim Brucker's website, a German version can be found there.

For both, Debian and Ubuntu, be careful not to install any other package of proofgeneral-misc than that from Brucker's repository. In newer linux distributions there may exist newer versions of ProofGeneral. Furthermore you will need to install the package xemacs21 in order to use xemacs.

Attention: The pacakge proofgeneral-misc (and proofgeneral) should have the version 3.6pre051004-0isamorph1!

Debian

  • Edit the file /etc/apt/sources.list by adding the following lines (replace stable with testing if you are using debian etch and with unstable if you are using debian sid)

    deb http://kisogawa.inf.ethz.ch/isamorph/debian stable main

    deb-src http://kisogawa.inf.ethz.ch/isamorph/debian stable main

  • Update your package manager by executing

    apt-get update

  • Install ProofGeneral (3.6pre051004-0isamorph1)

    apt-get install proofgeneral=3.6pre051004-0isamorph1 proofgeneral-misc=3.6pre051004-0isamorph1

  • Prevent overwriting ProofGeneral by a newer version

    echo "proofgeneral hold" | dpkg --set-selections

    echo "proofgeneral-misc hold" | dpkg --set-selections

  • Install Isabelle, XSymbol, FOL and HOL by executing

    aptitude install x-symbol isabelle isabelle-thy-hol isabelle-thy-fol

Ubuntu

The steps for Debian should also work for Ubuntu, but it is possible to do them with the synaptics package manager:
  • Start synaptic (System ⇒ Systemverwaltung ⇒ Synaptic-Paketverwaltung) and select settings ⇒ Repositories ⇒ Third-Party Software (Einstellungen ⇒ Paketquellen ⇒ Software von Drittanbietern). Add the two URLs

    deb http://kisogawa.inf.ethz.ch/isamorph/debian stable main

    deb-src http://kisogawa.inf.ethz.ch/isamorph/debian stable main

  • Close the dialog and click on Reload (Neu laden). Search and install the following packages:

    x-symbol

    isabelle

    isabelle-thy-hol

    isabelle-thy-fol

  • Search the packages proofgeneral and proofgeneral-misc, install the version 3.6pre051004-0isamorph1 from Brucker's repository and lock it. Use the menu "Package ⇒ Force Version" and "Package ⇒ Lock Version" ("Paket ⇒ Version erzwingen" and "Paket ⇒ Version sperren") for that step.

Windows

It is possible to install Isabelle on Windows using cygwin. An explanation can be found here:

http://web.abo.fi/~Viorel.Preoteasa/isabelle

Setup of ProofGeneral

On all systems you have to edit two files to set up the Isabelle mode in xemacs correctly
  • In the file /usr/share/emacs/site-lisp/proofgeneral/generic/proof-site.el uncomment (by removing the semicolons) the line

    (isa "Isabelle" "\\.ML$\\|\\.thy$")

  • In the file /usr/share/xemacs21/site-packages/lisp/site-start.el add the following line

    (setq isa-mode-map nil)

Now if you start xemacs and load a file with the extension '.ML' ProofGeneral should start automatically.