Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2016-RC2 Java exceptions related to se...


view this post on Zulip Email Gateway (Aug 22 2022 at 12:23):

From: Makarius <makarius@sketis.net>
On Fri, 29 Jan 2016, Eugene W. Stark wrote:

Since I started using Isabelle/JEdit (under Ubuntu), I have had issues
with the Search/Replace dialog. One that occurs very frequently is the
"Window must not be zero" exception. I just downloaded Isabelle2016-RC2
and since it has happened now nearly immediately with that, I am
reporting it. The stack trace is shown below. I don't have a
deterministic way to repeat it -- it just happens often while doing
search and replace, perhaps associated with the "No more matches found,
continue from the beginning" dialog.

Yes, looking at the corresponding Java sources of jEdit, it is indeed the
"keepsearching" dialog. But I don't think that jEdit is at fault.

java.lang.IllegalArgumentException: Window must not be zero
at sun.awt.X11.WindowPropertyGetter.<init>(WindowPropertyGetter.java:56)

Browsing through the world wild web, this exception occurs frequently in
trackers of Java/AWT/Swing projects like Netbeans, without any solution.
They usually say "wontfix" and point fingers back to Oracle.

It might be indeed one of these standard X11 window manager problems. The
Isabelle2016-RC2 Installation page specifies this intentionally as
follows: "Proper Window manager / Desktop environment that works with
Java/AWT/Swing".

You could try your luck openjdk-7 or openjdk-8 from the Ubuntu repository.
The resulting main directory is something like
/usr/lib/jvm/java-7-openjdk-amd64

It needs to be put in two places:

(1) $ISABELLE_HOME_USER/etc/settings:

ISABELLE_JDK_HOME="/usr/lib/jvm/java-7-openjdk-amd64"

(2) $ISABELLE_HOME/Isabelle2016-RC2.run near the end:

exec "/usr/lib/jvm/java-7-openjdk-amd64/jre/bin/java" \
...

For this Isabelle release, there is still a choice between Java 7 and 8 (I
think). We need to bundle Java 8 by default, since Oracle no longer
provides updates to its Java 7 distribution. It is unclear to me, which
one is worse or better.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:24):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I guess I will try what you suggest, however as additional data points
I was able to recreate the situation when I reloaded the same files,
both on Isabelle2016-RC2 and -RC1.

The situation seemed to be triggered by "Enter MATCH..." spew spamming
the output window. Apparently there was enough of it so that it filled
the JVM heap and perhaps caused continuous GC (speculation).
Eventually, poly became quiescent and presumably stopped sending output
to JEdit, but as I noted, JEdit did not recover, and after many minutes
I ended up killing it from the shell.

I also noticed upon restarting after killing that the first time JEdit
is restarted, it generates a "Failed to load Plugin" message, and does not
properly initialize. Upon exiting and starting once again, it starts
normally. So there is some state information that is retained somewhere
that prevents normal starting the first time after a crash or kill.

- Gene Stark

view this post on Zulip Email Gateway (Aug 22 2022 at 12:24):

From: Makarius <makarius@sketis.net>
I guess it actually refers to the thread "JEdit lockup with Java at 100%
CPU".

Since "Enter MATCH ..." is a formal "tracing" message, it should be
throttled according to system option editor_tracing_messages (default
1000), which is accessible in Plugin Options / Isabelle / General.

Did you change that option?

Another question is where these masses of "Enter MATCH ..." messages are
produced. It is normally some bad situation that can be avoided.

Makarius


Last updated: Apr 25 2024 at 04:18 UTC