Email Gateway (Aug 18 2022 at 19:26): Email Gateway (Aug 18 2022 at 19:26):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
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?
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?
Email Gateway (Aug 18 2022 at 19:27):From: Lawrence Paulson <lp15@cam.ac.uk>
It's clear that the intention is for everybody to migrate to jEdit eventually.
At the moment, I would say that PG is better for all-around usability. But it is hampered (it always has been) by the inherent instability of the Emacs layer that it sits on.
jEdit will be better when it has some sort of direct menu support for various Isabelle functions (sledgehammer, nitpick), display settings, et cetera. And it's to be hoped that somebody will write some sort of tutorial.
Larry Paulson
Email Gateway (Aug 18 2022 at 19:27):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 19:28):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Thank you for clarifying!
Email Gateway (Aug 18 2022 at 19:28):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Thank you for the explanation!
Last updated: Apr 26 2024 at 16:20 UTC
