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

If you want to use Isabelle on your computer (a linux system) at home, you should follow the instructions below.
  • Go to http://isabelle.in.tum.de/installation.html and follow the instructions
  • After the unpacking procedure switch to the ProofGeneral folder (e.g. "/usr/local/ProofGeneral")
  • Switch to the subfolder "generic" and edit the file "proof-site.el" with xemacs
  • Goto line 121 (beginning with the String ";; (isa")
  • Uncomment this line (remove the first two characters) and save
  • Use the Lisp compiler to recompile that file (in most cases xemacs comes with a main menu point "Lisp", choose "Byte-Compile This File")
  • Go to your working directory and type "Isabelle -I false ex26.ML", xemacs should appear starting ProofGeneral
  • Try to start Isabelle inside of ProofGeneral (just push the "GOTO" button or use the menu)
    (if you get an error which is related to "isa-mode-map" put the string "(setq isa-mode-map nil)" into the site-start.el (which is related to xemacs, try to find it in "/etc/emacs"), save and restart xemacs/Isabelle/ProofGeneral)