<- Back to the HOWTO section

Setup ProofGeneral and Isabelle

  • Audience: Scientists/Programmers who want to use Isabellewith ProofGeneral
  • Requires: MacPorts >=1.6


Setting up ProofGeneral and Isabelle can be tedious. This should provide some hints how to do to a setup with MacPorts.


Step 1: Install Isabelle

sudo port install isabelle

This will also install poly/ML for you.

Step 2: Install ProofGeneral

sudo port install ProofGeneral


Add the following lines to your ~/.emacs file:

; add the MacPorts path to the search path so that emacs will find isabelle and isatool
(setenv "PATH" (concat (getenv "PATH") "/opt/local/bin"))
(setq exec-path (cons "/opt/local/bin" exec-path))
; load the ProofGeneral configuration
(load-file "/opt/local/share/ProofGeneral/generic/proof-site.el")

Optional Parts

Depending on which version of Emacs you plan to use, add the following lines to ~/.emacs, too, to enable support for special symbols like quantors or the lambda symbol:

  • Carbon Emacs:
     '(isar-unicode-tokens-enable t)
     '(isar-x-symbol-enable nil)
     '(load-home-init-file t t)
     '(proof-three-window-enable t))
  • XEmacs, Emacs with GNOME/X11 bindings:
     '(isar-unicode-tokens-enable nil)
     '(isar-x-symbol-enable t)
     '(load-home-init-file t t)
     '(proof-three-window-enable t))

TODO: What else can be done?

  • Install e for sledgehammer

<- Back to the HOWTO section

Last modified 10 years ago Last modified on Jun 5, 2008, 10:25:24 AM