Before downloading Proof General, please register. It's free, it only takes a moment. If you have already registered you do not need to do so again.
You can join the Proof General mailing list for announcements of new versions. Developers and beta-testers may like to download a development release of Proof General. If you use an old version of a proof assistant and/or an old Emacs version, you may need to download one of the previous releases.
Proof General is distributed under the terms of
the
.
See below for software pre-requisites for running Proof General.
The next stable version of Proof General will be 3.4, to be released
in August. Until then, please try a
development release and
report any difficulties,
to help make the next release of Proof General as
robust as possible. Thanks!
To run Proof General, you must have:
There is also an optional component for using Proof General:
To use Proof General, simply unpack the sources with
tar xpzf ProofGeneral-3.4.tar.gz
(use gunzip first in place of z if you don't have
GNU tar),
and then add this one line to your .emacs file:
(load-file "directory/generic/proof-site.el")
Where directory is the directory in which you unpacked
the sources.
If you use the RPM package, directory is
/usr/share/emacs/ProofGeneral
If you're using Windows, then download the zip file.
Use a zip file utility to unpack it somewhere, for example
c:\ProofGeneral
Further customization is possible via the Customize menus in
Emacs.
See the
file in the distribution for more details.
X-Symbol is easy to install in XEmacs and configures itself automatically.
Simply download the binary package file, and do something like this to install in your home directory:
mkdir -p ~/.xemacs/xemacs-packages
cd ~/.xemacs/xemacs-packages
tar xpzf ../x-symbol-pkg.tar.gz
For GNU Emacs, you must remove the .elc files supplied, and add some code to your .emacs. See this page for details. More installation options are given in the the X-Symbol manual.