Re: [isabelle] Proof General of Isabelle/jEdit



On Mon, 30 Apr 2012, Aaron W. Hsu wrote:

So, I am just wondering whether I should be using the Isabelle/jEdit
interface or Proof General?  It seems like the jEdit interface is pretty
nice so far, but is it considered ready for prime time? Am I losing
anything really important in using the jEdit interface?

See http://en.wikipedia.org/wiki/File:Diffusionofideas.PNG -- it is up to you where you put sourself in the diagram, as "early adopter" or "laggard".

Starting with Isabelle2011-1, Isabelle/jEdit is officially marked as "stable", and in Isabelle2012 it will be again a bit more so. Certain conveniences of Proof General are still missing, and other Proof General features might never come, because they are just accidents imposed by the Emacs environment. (I have myself been there in 1999/2000 to help David Aspinall make Proof General work for Isabelle, and I still remember where Emacs side-conditions imposed certain ways that are no considered as inherent to the interaction model by Proof General power-users. There is are no plans to imitate Emacs features in Isabelle/jEdit.)


I guess, another question is what the intended "main" interface will be in the future? Is the intention to transition to the jEdit interface as the main one, or is it just a "newbie friendly" sort of thing?

Both Proof General and Isabelle/jEdit follow the idea that they don't make an a-priory distinction of targeting "newbies" and "power-users". It should be easy to get started and then continue for the hard work.

What will be the "main" interface depends on many factors. In the last 4 years only very few hands helped me in the daunting Isabelle/jEdit/PIDE project, so it will continue to move on slowly.

On the other hand, Isabelle Proof General is de-facto unmaintained for at least half a year now. So anybody still stuck with that needs to start thinking now ...


	Makarius





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