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 Oracle's Jdk).

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?

i3

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


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


	Makarius


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