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 inf.ed.ac.uk
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