This is a fork of PG that has support for Abella. Please follow the 'abella' branch.
Emacs Lisp Isabelle OCaml Coq Makefile Standard ML Other
Switch branches/tags
Nothing to show
Clone or download
Pull request Compare This branch is 10 commits behind ProofGeneral:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
acl2
ccc
coq
doc
easycrypt
etc
generic
hol-light
hol98
images
isar
lego
lib
obsolete
pghaskell
pgocaml
pgshell
phox
previous-art
twelf
.gitignore
.travis.yml
AUTHORS
BUGS
CHANGES
COMPATIBILITY
COPYING
FAQ.md
INSTALL
Makefile
Makefile.devel
Makefile.travis
README.md
REGISTER
pg-init.el
proof-general-pkg.el

README.md

Proof General — Organize your proofs!

Build Status

Overview

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.1~pre of Proof General.

About Proof General branches

Two editions of Proof General are currently available:

  • the (legacy) REPL-based, stable version of Proof General, gathered in the master branch, and licensed under GPLv2;
  • the (newest) Coq-specific, experimental version of Proof General, supporting asynchronous proof processing, gathered in the async branch, and licensed under GPLv3+.

Setup

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
(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

More info

See:

Links:

Supported proof assistants:

  • Full support for latest versions of: Coq
  • Support for previous versions of: 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.

Contributing

Contributions to this repository are placed under the BSD-3 license. As BSD-3 is compatible with both GPLv2 and GPLv3+, this means that we can merge them in both master and async branches if need be, using the same license as the rest of the codebase, while you keep all the rights on your code. For more info, see https://opensource.org/licenses/BSD-3-Clause.