The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think there should instead be a MELPA package, but, as I understand it, PG currently needs arcane emacs flags to compile correctly, and melpa doesn't support that (and it's not clear that it should).

However, making an opam package, if that's what you really want, should be trivial.

On Tue, Jan 19, 2016 at 1:11 AM, Gregory Malecha <gmalecha AT gmail.com> wrote:

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