Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Understanding Rewriting

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Understanding Rewriting


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Understanding Rewriting
  • Date: Thu, 09 Jul 2015 16:29:15 -0400



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




Archive powered by MHonArc 2.6.18.

Top of Page