[isabelle] Proof General as Coq-only front-end
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Proof General as Coq-only front-end
- From: Makarius <makarius at sketis.net>
- Date: Thu, 16 Jun 2016 00:00:49 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0
To whom it may concern.
Isabelle2014 (August 2014) is the last version that can still be used
with Proof General Emacs. On 31-Oct-2014 the last remains of the old TTY
loop have been removed. See also
especially the closing remark:
> It should be noted that the general PIDE protocol infrastructure is sufficiently flexibile to support old-fashioned stepping through proof scripts as well, maybe even with some Emacs front-end. So Proof General veterans who do care enough about that may assemble at the proofgeneral-devel mailing list to prove that this old warrior is not-quite-dead yet.
People who are still interested in Emacs have now a last chance to join
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel before all
old provers are removed, and Proof General becomes a Coq-only front-end.
I actually support that move: there is no point to keep obsolete prover
interfaces and prevent renovation of Proof General for the Coq-8.5
prover interaction protocol.
This archive was generated by a fusion of
Pipermail (Mailman edition) and