The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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