Organize your proofs!
Proof General is distributed under the terms of
GNU General Public License, Version 2.
See below for software pre-requisites for running Proof General.
tar xpzf ProofGeneral-4.2.tar.gz
Add this one line to your .emacs file, or inside its own file inside .emacs.d:
Where dir is where you unpacked the sources. This makes Proof General available whenever you launch Emacs.
The Makefile helps with further installation. Read INSTALL for details.
Important note: The tar file contains compiled files for GNU Emacs 23.2. To be sure of compatibility with a different version of Emacs you may need to recompile. To delete and recompile, use the provided Makefile being sure to set EMACS to point to your Emacs executable, e.g.:
make clean; make compile EMACS=/Applications/Emacs.app/Contents/MacOS/EmacsProof General will also run using the interpreted code, at some speed penalty.
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!
Please report problems and send fixes so we can maintain support for latest versions.