diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-02-12 16:38:08 -0500 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-02-12 16:39:46 -0500 |
commit | 1a3efed6d4eb2aff8b95648932ddf68c4f022f30 (patch) | |
tree | f3ed420f63265c135bc45262778e7133ada84c97 | |
parent | 942a4085d8b17b0be52d4e3c314fd6329a1aa8f5 (diff) |
A few clarifications in README
-rw-r--r-- | README.md | 20 |
1 files changed, 14 insertions, 6 deletions
@@ -8,23 +8,31 @@ This is version 4.4 of Proof General. ## Setup -Download and install Proof General from GitHub: +Remove old versions of Proof General, then download and install the new release from GitHub: ``` git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG -make -C ~/.emacs.d/lisp/PG +cd ~/.emacs.d/lisp/PG +make ``` -Then add the following to your .emacs: +Then add the following to your `.emacs`: ``` ;; Open .v files with Proof General's Coq mode (require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site") ``` +If Proof General complains about a version mismatch, make sure that the shell's `emacs` is indeed your usual Emacs. If not, run the Makefile again with an explicit path to Emacs. On Mac in particular you'll probably need something like + +``` +make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs +``` + ## More info See + INSTALL for installation details. COPYING for license details. COMPATIBILITY for version compatibility information. @@ -38,9 +46,9 @@ Links: Wiki: http://proofgeneral.inf.ed.ac.uk/wiki Lists: http://proofgeneral.inf.ed.ac.uk/mailinglist -Supported proof assistants: Coq, Isabelle, LEGO, PhoX -Experimental (less useful): CCC,ACL2,HOL98,Hol-Light,Lambda-Clam,Shell,Twelf - Obsolete instances: Demoisa,Lambda-Clam,Plastic +* Supported proof assistants: Coq, Isabelle, LEGO, PhoX +* Experimental (less useful): CCC,ACL2,HOL98,Hol-Light,Lambda-Clam,Shell,Twelf +* Obsolete instances: Demoisa,Lambda-Clam,Plastic A few example proofs are included in each prover subdirectory. The "root2" proofs of the irrationality of the square root of 2 were |