From 1a3efed6d4eb2aff8b95648932ddf68c4f022f30 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 12 Feb 2016 16:38:08 -0500 Subject: A few clarifications in README --- README.md | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index ca94b511..24477c8e 100644 --- a/README.md +++ b/README.md @@ -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 -- cgit v1.2.3