The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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.

Attachment: signature.asc
Description: OpenPGP digital signature