# Proof General: a generic Emacs front end for interactive proof assistants > Proof General is a GPL-3.0 Emacs Lisp package that gives proof assistants such as Coq, EasyCrypt, PhoX and qrhl-tool a shared editing and proof-running interface, with a stable REPL-based branch and an unmaintained asynchronous experiment. It suits a formal methods user who switches between provers, and it needs Emacs 25.2 or newer. **ProofGeneral/PG** — This repo is the new home of Proof General - Repository: https://github.com/ProofGeneral/PG - Website: https://proofgeneral.github.io - Stars: 562 · Forks: 109 - Language: Emacs Lisp - License: GPL-3.0 - Published: 2026-10-22 · Updated: 2026-10-22 · Language: en - Canonical page: https://hysenlabs.com/projects/proofgeneral-pg ## One editor for several provers, and the branch that decides which one Proof General is a generic Emacs interface for proof assistants, and the project's aim is stated as providing a powerful, generic environment for using interactive proof assistants. The generic part is the whole point. A formal methods researcher often uses more than one prover, because each has strengths, and the cost of switching is not the proofs but the tooling: the buffer layout, the goal display, the way you find a lemma, the way you name lemmas consistently, the way a script region is marked as a proof and sent to the prover. Proof General makes that layer common, so switching provers does not mean switching editors. There are two editions, and the distinction is about how the prover is driven. The standard, REPL-based, stable version is in the master branch, which is the default branch of the repository. The unmaintained Coq-specific, experimental version, which supports asynchronous proof processing, is in the async branch. That branch split is worth pausing on. An interactive prover talks to you: you send a fragment, it answers with goals and a status, and the buffer is updated in place. A REPL-based interface does that synchronously, one step at a time. Asynchronous proof processing would let the prover keep working while you edit, so a long-running step does not block the buffer. That is a much better experience, and it is also a much harder problem, because the buffer contents and the prover state can diverge. The project has an experimental implementation of it and calls it unmaintained, which tells you the experiment did not reach the point where it could replace the stable branch. The current version is 4.6-git, and the tagged releases are v4.5 from 2022-11-14 and v4.4 from 2016-09-18. The last push to the repository was on 2026-08-25, so the source is being worked on between releases. The licence is GPL-3.0, the primary language is Emacs Lisp, and the project is hosted at proofgeneral.github.io with the user manual and a separate adapting manual for people adding provers. ## Installing from MELPA, and the TLS setting that trips people up There are three install routes, and the package archives are the ones most people use. NonGNU ELPA is the sister repository of GNU ELPA and is enabled by default from Emacs 28 onwards, so if that repository is enabled you can install Proof General from it directly. MELPA is another repository of Emacs packages, and if you do not already use it you add the following to your .emacs and restart Emacs: ```elisp (require 'package) ;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t) (package-initialize) ``` The commented line in that snippet is the detail that catches people, and the documentation explains it well. If you have Emacs 26.1, which is precisely the packaged version in Debian 10, you may get the error message Failed to download 'melpa' archive during the package refresh step. This is a known bug, debbug #34341, which has been fixed in Emacs 26.3 and 27.1, and the workaround is to uncomment the gnutls-algorithm-priority line above. That is a nice example of documentation doing real work. The failure is a TLS negotiation problem in a package download, it names the exact error string, the exact Emacs versions affected, the upstream bug, and the one-line fix, which saves an afternoon. There is also a note for people moving from a manual installation to MELPA, to remove the old versions of Proof General from your Emacs context, either by removing the line loading PG/generic/proof-site from your .emacs or by uninstalling the proofgeneral package that your operating system's package manager provides. Two copies of the same package loaded at once is the kind of thing that produces confusing behaviour. Once MELPA is set up, you run M-x package-refresh-contents and then M-x package-install and type proof-general, which installs and byte-compiles the package. After that you can open a Coq file with the .v extension, an EasyCrypt file with .ec, a qrhl-tool file with .qrhl, or a PhoX file with .phx, and the corresponding major mode loads automatically. ## Building from Git, and the macOS Emacs path problem The manual route is a clone and a make, and the documentation is explicit that you remove old versions of Proof General first: ```sh git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG cd ~/.emacs.d/lisp/PG make ``` Then you add a single line to your .emacs: ```elisp ;; Open .v files with Proof General's Coq mode (load "~/.emacs.d/lisp/PG/generic/proof-site") ``` The Makefile is the place where the project structure shows through, and it is written by David Aspinall. The default target compiles the sources, there is a check target that compiles with warning flags enabled, a scripts target to edit the paths to bash, perl and PGHOME in the scripts, an install target that installs into system directories, a clean target that returns to clean source, and a tests target that runs the suite of regression tests. Two details in it are worth knowing. The PROVERS variable lists the subdirectories that are compiled and installed, which are coq, easycrypt, pghaskell, pgocaml, pgshell, phox and qrhl, and the generic Lisp code is in generic and lib, while the ADDITIONAL_ELISP variable holds code that is compiled but not installed, such as the compile tests under ci. So a prover instance is a directory, and whether it is a supported prover, an experiment, a shell instance or something obsolete is visible in the build configuration. There is also a second Makefile, Makefile.devel, for development work, and the install prefix defaults to /usr rather than /usr/local, with the comment explaining why: installs of desktop and doc files under /usr/local are unlikely to work with the rest of the system, and DEST_PREFIX and DESTDIR are there for staged installs such as building a Debian package. The Emacs executable is detected at build time, and the documentation warns about a specific failure. If Proof General complains about a version mismatch, make sure that the shell's emacs is indeed your usual Emacs, and if not, run the Makefile again with an explicit path to Emacs. On macOS in particular you will probably need something like: ```sh make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs ``` which is the standard Emacs packaging problem on a system where the app bundle is not the same binary as the one on the path, and it is easier to solve when the documentation names it in advance. ## Updating, and the supported prover list that keeps shrinking Keeping Proof General current follows the route you installed it from. For MELPA, updating all packages in one go is a package-list-packages, then r to refresh the package list, then U to mark upgradable packages, then x to execute the installs and deletions. For a Git installation in ~/.emacs.d/lisp/PG, the sequence is make clean, git pull, make, and the clean step matters because it removes the byte-compiled files that would otherwise be stale. The supported prover list is the part of the project that tells you about its history, and the documentation is unusually candid about it. The supported proof assistants are Coq, EasyCrypt, PhoX and qrhl-tool. Proof General used to support other proof assistants, but those instances are no longer maintained nor available in the MELPA package. The documentation then lists them by category. There was experimental support of Shell. There were obsolete instances, naming Demoisa. And there are removed instances, which is the long list: Twelf, CCC, Hol-Light, ACL2, Plastic, Lambda-Clam, HOL98, LEGO and Isabelle. Those names are a history of interactive theorem proving in one line, and the reason each was removed is instructive. Isabelle was removed because it has its own Emacs interface, which is the correct answer for a prover that ships one. The others were removed because their instances stopped being maintained, and an unmaintained prover instance in a shared package is a liability, since the interface protocol changes when the prover changes and nobody is there to update the adapter. The repository tree reflects the same history. There are directories for the supported provers, coq, easycrypt, phox and qrhl, the generic and lib directories for the shared code, the shell, Haskell and OCaml instances that are compiled but not installed, and then obsolete/, previous-art/ and resources/, which is where the removed material is kept. A few example proofs are included in each prover subdirectory, which is the practical way to see what a prover instance looks like when you are writing one. ## Where Proof General is the wrong tool The first limit is that it is Emacs-only, and not just Emacs but a recent-ish Emacs. It requires 25.2 or later, and the stated policy is to support multiple Emacs versions including those in Debian Stable and Ubuntu LTS until their End-Of-Support. A team standardised on another editor has no path to it, and a lab with a mix of editors ends up with two environments rather than one. The second is the price of the generic layer. Proof General gives every prover the same interface, which means the interface is a compromise. A feature that one prover has and another does not is either hidden or exposed awkwardly, and the buffer conventions, the goal display and the proof region marking are Proof General's, not your prover's. Users who love their prover's own Emacs mode, and Isabelle users are the obvious example since their instance was removed for exactly that reason, will find the generic layer a downgrade. The third is the state of the asynchronous branch. The idea is good and the implementation is labelled unmaintained, so the better interaction model is not available from this project today, and a user who wants a proof assistant that keeps working while they edit has to look elsewhere. The fourth is the maintenance of the prover instances themselves. The list of removed provers is a record of instances that decayed, and a user who picks a supported prover inherits a community-maintained adapter for it. When the prover changes its output format, the adapter has to change with it, and that work is invisible until it breaks. And the fifth is that installing is a little more work than a package. The MELPA route has the TLS edge case on older Emacs versions, the Git route needs a make with a possibly non-obvious Emacs path, and both need the earlier versions removed if they are present. None of that is hard, and all of it is friction that a user hits in the first ten minutes, which is where a tool wins or loses its audience. ## Conclusion Proof General is worth installing if you work in more than one proof assistant, because the buffer interface, the goal display, the proof script navigation and the lemma naming conventions are the same in all of them, so switching prover does not mean relearning the editor, and because the adapter architecture means a new prover is a configuration file rather than a new interface. It is the wrong tool if you use one prover and prefer its own front end. Before you set it up, check three things: that you pick the right branch, since master is the standard REPL-based stable version while the async branch is the unmaintained Coq-specific experimental version that supports asynchronous proof processing; that your Emacs is 25.2 or later and that your distribution's version is one the project still supports, with the policy aiming to cover Debian Stable and Ubuntu LTS until their End-Of-Support; and that you read the compatibility notes, because the repository carries a COMPATIBILITY file, a FAQ.md, an INSTALL file and a separate document for adapting PG to add provers, and the supported prover list has shrunk over time as instances became obsolete or were removed. ## FAQ ### How do I install Proof General in Emacs? The simplest route is MELPA: add (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t) to your .emacs, restart Emacs, then run M-x package-refresh-contents and M-x package-install and enter proof-general. NonGNU ELPA also works and is enabled by default from Emacs 28 onwards, and Proof General requires Emacs 25.2 or later. ### What is the difference between the master and async branches of Proof General? The master branch holds the standard, REPL-based, stable version of Proof General. The async branch holds the unmaintained Coq-specific experimental version that supports asynchronous proof processing, where the prover keeps working while you edit instead of one step at a time. ### Which proof assistants does Proof General support? The supported proof assistants are Coq, EasyCrypt, PhoX and qrhl-tool, and their file types .v, .ec, .phx and .qrhl load the matching major mode automatically. Proof General used to support more, but those instances are no longer maintained or are not in the MELPA package, with Demoisa listed as obsolete and Twelf, CCC, Hol-Light, ACL2, Plastic, Lambda-Clam, HOL98, LEGO and Isabelle listed as removed. ## Sources - [License: GPL-3.0](https://github.com/ProofGeneral/PG/blob/master/LICENSE) - [Project website](https://proofgeneral.github.io) - [ProofGeneral/PG on GitHub](https://github.com/ProofGeneral/PG) - [README](https://github.com/ProofGeneral/PG/blob/master/README.md) - [Releases](https://github.com/ProofGeneral/PG/releases) --- Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/proofgeneral-pg