The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

This is great. Will there be an opam package for this?

On Mon, Jan 18, 2016 at 7:56 PM, Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

Hi Coq-club,

I'm happy to announce that the development of Proof General has moved to GitHub [1]. Proof General was created by David Aspinall [2], and its Coq plugin is currently maintained by Pierre Courtieu.
With the imminent release of Coq 8.5, I'd like to encourage Proof General users to give the updated Proof General a try; it should be fully compatible with both the latest 8.4, and the upcoming 8.5. Installing it is fairly easy (you'll need to uninstall the packaged version for your OS distribution, if you use one):

  git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
  make -C ~/.emacs.d/lisp/PG

Then add Proof General to your .emacs:

  (require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site")

Please report issues with this new version of the GitHub tracker, and let us know if we could make Proof General better! Contributions in the form of patches or pull requests are also very welcome.

[1] https://github.com/ProofGeneral/PG
[2] Aspinall, D. (2000). Proof General: A generic tool for proof development. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 38-43). Springer Berlin Heidelberg.

--

gregory malecha