Join the Proof General mailing list for announcements of new versions.
Quick installation instructions
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
;; Open .v files with Proof General's Coq mode (load "~/.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 macOS in particular you’ll probably need something like
make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
- A proof assistant, e.g.: Coq, Isabelle/Isar, LEGO, PhoX (see links for versions).
- Version 24.3 or later of GNU Emacs.
Emacs is available for a huge variety of platforms, including Unix, Windows, and macOS. See the Emacs Wiki for advice.
Compatibility across the multitude of platforms, provers and Emacs versions is very troublesome as invariably things break with Emacs or prover API changes and new bugs. You may have luck with older versions but there are no guarantees!
If you have an old version of a proof assistant and/or an old Emacs version, you may need a previous release of Proof General:
- http://proofgeneral.inf.ed.ac.uk/oldrel.php (up to Proof General 4.0)