Re: [isabelle] Isabelle2014 and ProofGeneral

On Sat, 13 Sep 2014, Ian Zimmerman wrote:

Makarius> To disprove that, are you willing to do anything yourself?
Makarius> Today it would mean doing a few reforms in the Emacs LISP
Makarius> implementation to work directly with Isabelle process protocol
Makarius> functions, not the obsolete Isar TTY toplevel anymore.

I hope the "today" is not literal, but soon, Yes.  I am here to help.

Makarius> If there are no hard facts showing up to continue classic
Makarius> Proof General Isabelle support one more season, it will be
Makarius> removed without further ado in the next Isabelle release.

By "classic" do you mean "TTY"?

Classic means the current "optional" Proof General component with its use of the obsolete TTY loop. That is in the way for a long time, and it is about to disappear soon.

So if the new work is successful PG lives on?  Deal.

I am not even required in that deal.

The regular Isabelle process interface provides official ways to define protocol functions, and thus implement front-ends in user-space without the old TTY loop. Thus it should be relatively easy to re-implement old PG interaction, although the relative weak Emacs LISP infrastructure might require some tricks to make it work.

Anything else should be discussed on the proofgeneral-devel at

For instance, will it now start working magically in the background instead of synchronously?

It depends how this is done. Nothing of that is hard-wired into Isabelle. Old-fashioned synchronous interaction can be implemented independently of the PIDE interaction model.

Now to return to my immediate problem, after I register the PG component, do I still need the "emacs" script? I think this might be the case from reading the other thread. If yes this would be a handy bit of information to put in the NEWS file.

The NEWS file provides all relevant entry points. On the other thread, Lars Noschinski also provided concrete examples how to apply that information in practice.

Isabelle components are well-documented, although this knowledge is not required by default for regular Isabelle releases. In Isabelle2014 the defaults have been changed such that Proof General users have to stand up and do some tiny bit of work by themselves, just as a symbolic gesture.


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