Skip to content

DavidAspinall/PG

 
 

Repository files navigation

Proof General — Organize your proofs!

Build Status

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.

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.

About

This repo is the new home of Proof General

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Emacs Lisp 81.2%
  • Isabelle 8.7%
  • OCaml 4.7%
  • Coq 1.6%
  • Makefile 1.3%
  • Standard ML 1.0%
  • Other 1.5%