The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

I could write an opam file for it. I think it would be suitable, but I think that there are aptitude, and emacs package descriptions for it as well, and together it's confusing which route to take and all...

On Thu, Jul 9, 2015 at 4:29 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 07/09/2015 04:05 PM, Kenneth Adam Miller wrote:

Yes, I'm using ProofGeneral. I'm not sure how I installed it off the top of
my head... I'd like to use some kind of package manage to facilitate
keeping it up to date. Are there instructions anywhere to follow to make
sure that the install of proof general goes well?

I followed the "CVS access" section of http://proofgeneral.inf.ed.ac.uk/devel.  The INSTALL file in the CVS top level has the necessary instructions.  I think things work best with an Emacs version >= 24.3.

As far as package managing PG - note that the released PG version (4.2) is very out of date with respect to Coq.  Also, even though some linuxes see more recent releases, they're still considerably out-of-date - for instance, version 4.3~pre130510-1 is in the debian jessie/sid repos - but that's still more than 2 years old.  I don't know if there are other avenues to manage more recent versions other than the gzip'ed tar file on http://proofgeneral.inf.ed.ac.uk/devel (which is only slightly out of date, but not reliably so), or dealing with the CVS repo.

I don't know if the new opam-based management for Coq contains a copy of PG.

-- Jonathan