[isabelle] Proof General as Coq-only front-end



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
http://sketis.net/2014/discontinuation-of-isabelle-proof-general --
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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.