Changes between Version 1 and Version 2 of howto/SetupProofGeneral

Timestamp:

Jun 5, 2008, 10:25:24 AM (16 years ago)

Author:

mww@…

Comment:

--

howto/SetupProofGeneral

@@ -3 +3 @@
 = Setup ProofGeneral and Isabelle =
 
- * Audience: TODO
- * Requires: MacPorts >=TODO
+ * Audience: Scientists/Programmers who want to use Isabellewith ProofGeneral
+ * Requires: MacPorts >=1.6
 
 == Introduction ==
 
-TODO
+Setting up ProofGeneral and Isabelle can be tedious. This should provide some hints how to do to a setup with MacPorts.
 
 == Installation ==
 
-=== Step 1: '''TODO: Step 1 title''' ===
-
-TODO
+=== 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 ==
 
-TODO
+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]