Version 2 (modified by mww@…, 16 years ago) (diff) |
---|
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