Proof General is a generic Emacs interface for proof assistants. The aim of the Proof General project is to provide a powerful, generic environment for using interactive proof assistants.
This is version 4.4 of Proof General.
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
cd ~/.emacs.d/lisp/PG
make
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
See
INSTALL for installation details.
COPYING for license details.
COMPATIBILITY for version compatibility information.
REGISTER for registration information (please register).
FAQ, doc/ for documentation of Proof General.
<prover>/README for additional prover-specific notes
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
A few example proofs are included in each prover subdirectory. The
"root2" proofs of the irrationality of the square root of 2 were
proofs written for Freek Wiedijk's challenge in his comparison of
different theorem provers, see http://www.cs.kun.nl/~freek/comparison/.
Those proof scripts are copyright by their named authors.
(NB: most of these have rusted)