Discontinuation of Isabelle Proof General

31-Oct-2014 is the historic date (Reformation Day!) when support for Proof General was ultimately removed from the Isabelle code base. This is the relevant changeset.

This means the current official release of Isabelle2014 (August 2014) is the last one where Proof General Emacs is still available as (optional) component; see the explanation in the published NEWS. After that its 15 years of history comes to an end, with the last 3 years an increasingly heavy burden and hindrance of further advances in Prover IDE technology (as represented by Isabelle/jEdit).

The TTY loop for the Isar toplevel has been removed as well, see changeset. It might appear rather drastic to have an Interactive Theorem Prover without the classic read-eval-print loop, but we need to recall that TTY interaction stems from the 1970-ies.
PIDE supports direct editing of theory documents as interactive sessions (or projects): this is more adequate for the interaction standards of the 1990-ies — a form of direct manipulation.

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.

Flattr this!