Re: [isabelle] Remaining reasons for Proof General
On Mon, 11 Nov 2013, René Neumann wrote:
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).
The hardware is OK. Since this is Intel hyperthreading, you might want to
experiment with explicit option threads=4 instead of the default 8.
Running on Linux, you can spoil the performance game by graphics drivers,
or other Gtk-specific oddities that I can't pin down. Java/Swing
applications only work well on a moderately configured mainstream Linux
systems. Being aggressively Linux-oid spoils the game. OpenJdk also does
not really help in this respect (the code base is mostly the same as
Users of Windows and Mac OS X have an inherent advantage here.
- (obsolete: my WM fails to show jEdits dialogs. Just noticed that there
is a patch available for it).
What is your WM?
Never heard of that. Consider it unsupported.
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).
This is a very old argument of WM guys versus Java guys. They hate each
other for that and accuse the other side of being wrong.
I've recently done some research of relevant AWT sources and corresponding
OpenJdk mailing list threads. I can't tell if and when the situation will
improve. Oracle is fighting at too many fronts at the same time.
For Isabelle/jEdit, I declare this issue as off-topic. Users need to use
a well-known WM -- or join the OpenJdk project to solve the problem
- 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>.
The completion mechanism of Isabelle2013-1 works quite nicely with such
things. I've spent several weeks just on these details.
This archive was generated by a fusion of
Pipermail (Mailman edition) and