Re: [isabelle] Remaining reasons for Proof General



Am 11.11.2013 18:13, schrieb Makarius:
> 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.

Quadcore i7. Which should be fast enough... I'm using the gtk-style for
jEdit. Or I would need a high-end GPU ... (intel-whatever here only).

New testing on a second machine (which is slower) does not yield any
lags. Strange. Have to investigate.
> 
>> - 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.

Thanks. This indeed does work now.

> 
>> - 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.

My use case: Using PG with session X. Then noticing that I had to change
some theory in X. With session switching this was easy: Exit Isabelle,
switch session, restart isabelle (thereby building all of session X, but
for development this is ok).

With jEdit I would have to restart the editor.

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

i3

> 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.

That's not a solution, but a workaround (I'm using the WM I'm using for
good reasons). The problem is not the WM, but Java, as it changed
behavior in Java7 and a new workaround in the WM had to be developed
(again: why Java is not just using existing techniques/libraries and is
doing everything from scratch itself, I do not understand).

But as already written: This problem is obsolete until the next JDK version.

> 
>> - 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.

Typing e.g. /\ and getting \<and>, or |/ and getting \<^sub>.


But I just ran a fresh download on a previously isabelle-free computer
and it looked better than expected. Hence I'll give it a fresh try at
work (after having patched by WM) and will come back tomorrow (I'll also
ditch the gtk-style)

- René




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