Dear Proof General developers,

we are presently in the phase of testing release candidates for Isabelle2015, which is scheduled for the end of May (or start of June) 2015. See also

One notable item in the NEWS for this release:

  * Support for Proof General and Isar TTY loop has been discontinued.
  Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.

I did this already shortly after the release of Isabelle2014, which is the last Isabelle release with Proof General and TTY loop support. See also

The removal of TTY interaction was a great relieve to the Isabelle system implementation, and opened up many opportunities for reforms that were unthinkable before.

Since Isabelle no longer works with Proof General, you may consider liberating the Proof General code base from the corresponding modules, and thus maybe move forward as well.

An alternative scenario was sketched on the above blog entry in 15-Nov-2014:

  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.

While it is technically feasible to connect Proof General to Isabelle/Scala/PIDE in some imitation of the old TTY mode, I personally don't believe that there are serious adherents to Emacs still around to do that.

ProofGeneral-devel mailing list

Reply via email to