Email Gateway (Aug 19 2022 at 11:41): Email Gateway (Aug 19 2022 at 11:41):From: Leo Freitas <leo.freitas@newcastle.ac.uk>
Hi,
I am getting a frequent crash of Isabelle/jEdit with the following error
"
/Applications/Isabelle2013.app
/Contents/Resources/Isabelle2013/lib/Tools/java: line 1:
375 Trace/BPT trap: 5
"$ISABELLE_JDK_HOME/bin/$PRG" "$@"
Return code: 133
"
It seems to happen every time a set of theories are loaded. Any hint / suggestion on what's happening?
Could send the larger log if needed.
Many thanks
Leo
Email Gateway (Aug 19 2022 at 11:42):From: Makarius <makarius@sketis.net>
On Fri, 23 Aug 2013, Leo Freitas wrote:
I am getting a frequent crash of Isabelle/jEdit with the following error
"
/Applications/Isabelle2013.app
/Contents/Resources/Isabelle2013/lib/Tools/java: line 1:
375 Trace/BPT trap: 5"$ISABELLE_JDK_HOME/bin/$PRG" "$@"
Return code: 133
"It seems to happen every time a set of theories are loaded. Any hint /
suggestion on what's happening?
When there is a crash, the first thing is to look closely what has crashed
and who is responsible for it, and what can be done about it.
Isabelle/jEdit is a plain Scala/JVM application without native libraries,
so its own crashes would be just long JVM-style exception traces.
Sometimes the underlying Isabelle/ML process may crash, which is then
a matter of telling David Matthews, who is the wizard behind that system.
Above the crash is due to bin/java, which means it is a problem by Oracle
and Apple -- which are sometimes like Gozilla vs. King Kong fighting each
other, but both have sufficient software quality problems on their own to
work on.
There might be workarounds via JVM options (e.g. Isabelle settings
JEDIT_JAVA_OPTIONS or JEDIT_SYSTEM_OPTIONS) or juggling different JVM
versions. We should sort this out off-list via private mail, and report
the final result here if it is relevant for general public. (In any case,
I usually distill from such incidences certain parameters to go into the
next official Isabelle release.)
Could send the larger log if needed.
Yes, please send me that privately.
Makarius
Email Gateway (Aug 19 2022 at 11:43):From: Tobias Nipkow <nipkow@in.tum.de>
I think this is a general problem of the JVM on Macs. I frequently get it when I
close the lid of my Mac and reopen it...
Tobias
Email Gateway (Aug 19 2022 at 11:43):From: Makarius <makarius@sketis.net>
We should try to collect and pin down such incidents.
I occasionally get something like that on a "cold start", e.g. when using
my MacBook Pro for presentations (when it runs Mac OS X and not Ubuntu)
and starts the JVM for the first time. This makes a 50% chance of core
dump of bin/java. When giving the Isabelle tutorial at Edinburgh this
May, where Leo was also present, I had several such "crashes on stage".
Oracle and Apple are to blame, but we should try to find workarounds.
Lets first see what the more drastic crash that Leo has encountered tells
us about these raw industrial materials.
Makarius
Email Gateway (Aug 19 2022 at 11:43):From: Makarius <makarius@sketis.net>
Just one speculative idea, before we walk through your crash logs.
Isabelle2013/lib/Tools/java invokes the "java" executable with option
"-server" to make the code faster over time. This quite aggressive
just-in-time compilation might interfere with normal running of the code
-- it somehow conforms to the observations about "cold-start problems"
that I have described on this thread already.
So removing the "-server" mode or saying "-client" explicitly might make a
difference in robustness, at the cost of some runtime performance.
Makarius
Last updated: Apr 24 2024 at 01:07 UTC