Re: [isabelle] Remaining reasons for Proof General



On Mon, 11 Nov 2013, René Neumann wrote:

Am 11.11.2013 12:34, schrieb Makarius:
People who are still using Proof General should say more explicitly what
are the reasons for it,

I think, I had put it in another mail already, but well:

IIRC, that was for Isabelle2013. So for Isabelle/PIDE 3rd generation. Now we have Isabelle2013-1 and the 4th generation.

One of the big differences to Proof General is that there are big differences in each release cycle. You really need to look what is there
everytime afresh.


- jEdit is SLOW, as in: There is a noticeable lag when moving from one menu to the other per mouse (rendering also consumes 50% to 100% of one CPU).

What is your hardware like? I usually see 20% total time for the JVM and approx. 400-800% for Isabelle/ML. That is an old 8 core machine from 2009.

Java has this odd feature that it sometimes "looks slow", but it actually isn't.

Isabelle/jEdit was started in 2008 to make efficient use of current hardware (2 cores or more).


- Fonts are not antialiased. I found that setting some obscure environment variable [1] made it work, but honestly: no AA by default is a no-go.

Obsolete in Isabelle2013-1 and hardly an issue before, since it was well documented in the jEdit FAQ how to change such defaults.


- no switching of sessions (at least last time I checked)

Rarely needed, unless you make a convincing point for such a marginal feature. In Isabelle/jEdit you can load disjoint sessions without interfering each other.

Proof General legacy support is actually in the way to clean up all that and make just one way of Isabelle build or Isabelle/jEdit with multiple sessions.


- (obsolete: my WM fails to show jEdits dialogs. Just noticed that there
is a patch available for it).

What is your WM? There are many Linux guys who just don't want Java applications on their particular fork. The solution is to use one of the well-known standard window managers.


- jEdit is too mouse-centric. When I have to use "Ctrl-hover" to get
some information, I won't use it.

You don't even have this functionality in Proof General, so it is hardly
a remaining reason for Proof General.

Again: after some weeks of practice, you will be much faster with jEdit than Emacs. I always feel encumbered when I have to go back to Emacs for some reason.


- last time I checked, the 'abbreviation to unicode' conversion that
finally(!!) works great in PG, was somewhat unusable in jEdit.

Can you explain that feature of Proof General.  I have never heard of it.

In Isabelle2013-1 the symbol completion mechanism has been generally brushed up. Better forget what it was in Isabelle2013 or Proof General, and experiment to see its possibilities. There is also some documentation in the Isabelle/jEdit manual.


apart from old habits.

And this is also not to be underrated. Over the last two years, I have compiled a 150 lines .emacs (and I'm only using Emacs for Isabelle) plus some 'isabelle emacs' startup magic. Hence being urged to spend all this time again to get the editor in a shape one likes, does not feel good. Especially when there are NEWS items reading "you have to re-do all your current jEdit keybinding customizations".

I can't do anything here. You need to be ready to give up old Emacs things and move on to a brave new world. Isabelle/jEdit is not the future, it is the present for quite some time already.


	Makarius


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