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.
Download and install Proof General from GitHub:
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
make -C ~/.emacs.d/lisp/PG
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")
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)