Email Gateway (Aug 22 2022 at 13:36): Email Gateway (Aug 22 2022 at 13:36):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC