[wiki:howto <- Back to the HOWTO section]

= Setup ProofGeneral and Isabelle =

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

== Introduction ==

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

== Installation ==

=== Step 1: '''Install Isabelle''' ===
{{{
sudo port install isabelle
}}}
This will also install poly/ML for you.
=== Step 2: '''Install ProofGeneral''' ===
{{{
sudo port install ProofGeneral
}}}

== Configuration ==

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:
{{{
(custom-set-variables
 '(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:
{{{
(custom-set-variables
 '(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

[wiki:howto <- Back to the HOWTO section]