Re: [isabelle] Isabelle2014 and ProofGeneral
Makarius <makarius at ...> writes:
Ian> I have read that thread now, thanks. I disagree with most of what
Ian> you say there, but I can see there's no changing your position, so
Ian> I will resist the urge to jump in.
Makarius> This strange game around Proof General is already quite old.
Makarius> De-facto, I am the only one who ever invested serious work in
Makarius> its Isabelle connectivity, and there were many calls to action
Makarius> to continue that by someone else after the start of PIDE in
Makarius> 2007/2008. Nothing has ever happened, though. Proof General
Makarius> users are characterised by inactivity.
I think what happened is that David A., the main PG developer, had a
conversion similar to yours (but in his case to eclipse rather than jedit).
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"? So if the new work is successful PG
lives on? Deal. I have a reservation, though: will this fundamentally
change the feel of Isabelle/PG? For instance, will it now start working
magically in the background instead of synchronously?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and