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
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 ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and