Re: [isabelle] Isabelle2014 and ProofGeneral



On Sat, 13 Sep 2014, Ian Zimmerman wrote:

I have read that thread now, thanks. I disagree with most of what you say there, but I can see there's no changing your position, so I will resist the urge to jump in.

This strange game around Proof General is already quite old. De-facto, I am the only one who ever invested serious work in its Isabelle connectivity, and there were many calls to action to continue that by someone else after the start of PIDE in 2007/2008. Nothing has ever happened, though. Proof General users are characterised by inactivity.

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

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


	Makarius




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