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 MHonArc.