coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, John Wiegley, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Abhishek Anand, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Jonathan Leivent, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Jonathan Leivent, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Vadim Zaliva, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, Pierre Courtieu, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, Clément Pit--Claudel, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Jonathan Leivent, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Abhishek Anand, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Emilio Jesús Gallego Arias, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, John Wiegley, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, Hugo Herbelin, 07/12/2015
- Re: [Coq-Club] Understanding Rewriting, John Wiegley, 07/12/2015
- Re: [Coq-Club] Understanding Rewriting, Hugo Herbelin, 07/12/2015
- Re: [Coq-Club] Understanding Rewriting, Hugo Herbelin, 07/12/2015
- Re: [Coq-Club] Understanding Rewriting, John Wiegley, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, Hugo Herbelin, 07/11/2015
- Re: [Coq-Club] Understanding Rewriting, John Wiegley, 07/09/2015
Archive powered by MHonArc 2.6.18.