Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sluggish Isabelle/jEdit experience with extern...


view this post on Zulip Email Gateway (May 23 2024 at 09:18):

From: Makarius <makarius@sketis.net>
Can anybody confirm this behaviour, e.g. with a single display and very large
editor view and/or small font?

I cannot really reproduce it, although I see a small slowdown (factor 1.2) of
text area painting after moving from Java 17 to Java 21 (Isabelle/4fb5e6499da9).

My test environment: Macmini M1 with macOS 14.4.1 and two 4K-displays (HDMI
and DisplayPort).

Makarius

view this post on Zulip Email Gateway (May 23 2024 at 10:11):

From: "John F. Hughes" <jfh@cs.brown.edu>
I've just tested this on a 2015 Macbook

Model Name: MacBook Pro

Model Identifier: MacBookPro12,1

Processor Name: Dual-Core Intel Core i5

Processor Speed: 2.9 GHz

Number of Processors: 1

Total Number of Cores: 2

L2 Cache (per Core): 256 KB

L3 Cache: 3 MB

Hyper-Threading Technology: Enabled

Memory: 16 GB

System Firmware Version: 481.0.0.0.0

OS Loader Version: 540.120.3~37

SMC Version (system): 2.28f7

using two displays, one Thunderbolt using DP, the other a Dell U2715H using
HDMI, both using "Default for display" resolution.

It's a bit slow (i.e., copy-pasting 2048 lines to get to 4096 took a
half-second or so, and then processing them all took 38 seconds), but the
UI repainting, etc., seemed pretty good even when there were those 4.1K
lines --- it almost kept up with my typing in a new theorem at the bottom
of the file (if x is a positive natural number, then so is 2x), although it
reminded me a little of the 300-baud modem days...I could type ahead a
bit if I tried. And it took 14 seconds for "using assms by auto" to be
accepted as a proof.

Frankly, all that seems like the limitations of this 9-year-old laptop
rather than the software.

I saw no difference in performance between the Thunderbolt screen and the
Dell screen.

view this post on Zulip Email Gateway (May 23 2024 at 23:55):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
I can confirm that behaviour on a recent M3 MacBook Pro + 5k external Thunderbolt Display + MacOS 14.5 + Isabelle2024-RC3. On the laptop screen, the UI is very responsive and fast (faster than on any other machine I have), on the external display scrolling for instance is sluggish in normal use and does show the described symptoms for that specific lemma above repeated about 2000 times. The delay is not long, but noticeable enough to be annoying.

This completely goes away if I move the same window over to the laptop screen.

It does seem to be resolution dependent — if I manually reduce the resolution to something smaller on the external monitor, performance increases. Font size doesn’t seem to make a difference.

The same happens to a lesser extent with a different external 4k monitor over USB-3. On that one I can still see a difference to the internal display, but the delay is no longer that annoying. The resolutions it shows me are

(it runs all of these in double resolution in reality)

It doesn’t seem to matter whether both external screens are connected or not. If I extend the display via wifi to an iMac with 1920x1080 (x2) resolution, it performs better than the directly connected external 5k display (but still slower than the directly connected 4k display, of course).

I do not observe that behaviour with other programs/editors, e.g. Safari or VSCode are both smooth and fast on the external displays.

This also does not happen with Isabelle2023. The UI is normally responsive there on the external display.

If I had to guess I would suspect something going wrong with Java and graphics hardware acceleration.

Cheers,
Gerwin

view this post on Zulip Email Gateway (May 24 2024 at 09:26):

From: Makarius <makarius@sketis.net>
Your guess is probably correct. Someone else has pointed to the following
ticket on a private thread: https://bugs.openjdk.org/browse/JDK-8284378

"""
JEP 382 - macOS Metal Rendering Pipeline for Java 2D was delivered in JDK 17,
but it is OFF by default, and OpenGL remains the default rendering pipeline.
Having worked through the critical issues which are specific to the Metal
pipeline, and having it available in two releases of JDK already, it is time
to make Metal the default pipeline.

The benefits should be that the more modern Metal API will be more stable
going forward, be more power friendly, faster on most operations, and will
benefit from increased focus on Metal in future Apple hardware.

It will require macOS 10.14 or later - and all systems capable of running
macOS 10.14 and later automatically support metal.
To the remaining extent that JDK is supported or even functional on macOS
10.13 and earlier, they will continue to remain using OpenGL.

Reversion to OpenGL will be possible so long as it is supported by specifying
-Dsun.java2d.opengl=true as a system property on the command line.
"""

Maybe owners of very high-end Apple hardware can test that and report on the
results.

Makarius

view this post on Zulip Email Gateway (May 26 2024 at 01:39):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>

On 24 May 2024, at 19:26, Makarius <makarius@sketis.net> wrote:

"""
[..]
Reversion to OpenGL will be possible so long as it is supported by specifying -Dsun.java2d.opengl=true as a system property on the command line.
"""

Maybe owners of very high-end Apple hardware can test that and report on the results.

Can confirm that adding -Dsun.java2d.opengl=true to JEDIT_JAVA_OPTIONS gives me the fast Isabelle2023 behaviour on the external display.

Cheers,
Gerwin

view this post on Zulip Email Gateway (May 26 2024 at 09:26):

From: Clemens Ballarin <ballarin@in.tum.de>
Glad to hear that this helps.

Please consider reporting the issue to
https://bugs.java.com/bugdatabase/, perhaps after enquiring on
https://mail.openjdk.org/mailman/listinfo/client-libs-dev how to best
proceed in this case.

Clemens


Last updated: Jan 04 2025 at 20:18 UTC