Email Gateway (Aug 22 2022 at 13:40): Email Gateway (Aug 22 2022 at 13:40):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I experience this type of failure on the next start up after having
terminated Isabelle abnormally (e.g. by killing the process). When the
failure occurs, exiting JEdit and restarting Isabelle results in a normal
startup. There is evidently some state information that is used on startup
that is not left in the proper condition on an abnormal shutdown.
(I use Isabelle on Ubuntu 14.04LTS using the default Unity window manager.)
Could it be that the failures you are seeing are the result of abnormal
shutdowns of the immediately preceding sessions?
- Gene Stark
Email Gateway (Aug 22 2022 at 13:40):From: Hans-Jörg Schurr <lists@schurr.at>
Hello everyone,
I have encountered this error too. In my case it appears reproducible
when Isabelle is not shut down normally. E.g. when the machine crashed
or the editor window is killed via xkill. After a restart Isabelle works
normally.
Hope this helps,
Hans-Jörg
Email Gateway (Aug 22 2022 at 13:41):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Eugene, Hans-Joerg,
Could it be that the failures you are seeing are the result of abnormal
shutdowns of the immediately preceding sessions?
It may very well be, though I admit I haven't been paying enough
attention to confirm one way or the other! Hans-Joerg's e-mail seems
to suggest that this is a likely cause, however.
Thanks,
Dominic
Email Gateway (Aug 22 2022 at 13:42):From: Makarius <makarius@sketis.net>
Studying all mails on this thread again, I am unsure if the problems are
necessarily related.
The general situation is that Isabelle application startup needs to load
and warm-up many jars. If anything goes wrong, e.g. due to network
file-system errors, bad things might happen.
I am not really an expert on the JVM, even after almost 10 years of
using it routinely. jEdit has its own tricks for class loading, but this
is only for the topmost plugin container, not the underlying Scala
libraries -- these are loaded before jedit.jar itself.
To rule out accidental problems with a particular JVM version, I've made
the following alternative application bundles of Isabelle2016 with old
but stable jdk-7u80 and newly updated jdk-8u102:
http://www4.in.tum.de/~wenzelm/test/Isabelle2016_jdk-7u80
http://www4.in.tum.de/~wenzelm/test/Isabelle2016_jdk-8u102
After the summer, we will be heading again towards the next Isabelle
release (before the end of the year).
It would be nice if known JVM instabilities are clearly isolated and
eliminated until then.
Makarius
Email Gateway (Aug 22 2022 at 13:42):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
What I am easily and reliably able to reproduce is as follows:
% /opt/Isabelle2016/Isabelle2016 &
(wait for Isabelle to start)
% kill -KILL 29909 # or whatever the PID is of the Java process
[1] + Killed /opt/Isabelle2016/Isabelle2016
% /opt/Isabelle2016/Isabelle2016&
[1] 9015
% 7:40:39 AM [main] [error] PluginJAR: Error while starting plugin isabelle.jedit.Plugin
7:40:39 AM [main] [error] PluginJAR: java.lang.NoClassDefFoundError: scala/Function0
7:40:39 AM [main] [error] PluginJAR: at java.lang.Class.getDeclaredConstructors0(Native Method)
7:40:39 AM [main] [error] PluginJAR: at java.lang.Class.privateGetDeclaredConstructors(Class.java:2671)
7:40:39 AM [main] [error] PluginJAR: at java.lang.Class.getConstructor0(Class.java:3075)
7:40:39 AM [main] [error] PluginJAR: at java.lang.Class.newInstance(Class.java:412)
7:40:39 AM [main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:933)
7:40:39 AM [main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePluginIfNecessary(PluginJAR.java:1021)
7:40:39 AM [main] [error] PluginJAR: at org.gjt.sp.jedit.jEdit.main(jEdit.java:549)
7:40:39 AM [main] [error] PluginJAR: Caused by: java.lang.ClassNotFoundException: scala.Function0
7:40:39 AM [main] [error] PluginJAR: at java.net.URLClassLoader.findClass(URLClassLoader.java:381)
7:40:39 AM [main] [error] PluginJAR: at java.lang.ClassLoader.loadClass(ClassLoader.java:424)
7:40:39 AM [main] [error] PluginJAR: at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:331)
7:40:39 AM [main] [error] PluginJAR: at java.lang.ClassLoader.loadClass(ClassLoader.java:357)
7:40:39 AM [main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadFromParent(JARClassLoader.java:518)
7:40:39 AM [main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:87)
7:40:39 AM [main] [error] PluginJAR: at java.lang.ClassLoader.loadClass(ClassLoader.java:357)
7:40:39 AM [main] [error] PluginJAR: ... 7 more
7:40:39 AM [main] [error] ErrorListDialog$ErrorEntry: /opt/Isabelle2016/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
7:40:39 AM [main] [error] ErrorListDialog$ErrorEntry: Cannot start: java.lang.NoClassDefFoundError: scala/Function0
7:40:39 AM [main] [error] ErrorListDialog$ErrorEntry: Try updating to a newer version of the plugin.
7:40:39 AM [main] [error] View: No docking framework PIDE available, using the original one
7:40:43 AM [AWT-EventQueue-0] [error] DockableWindowManagerImpl: Unknown dockable window: isabelle-output
7:40:43 AM [AWT-EventQueue-0] [error] DockableWindowManagerImpl: Unknown dockable window: isabelle-theories
JEdit displays a "Plugin Error" pop-up that says:
/opt/Isabelle2016/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start: java.lang.NoClassDefFoundError: scala/Function0
Try updating to a newer version of the plugin.
(Click on OK)
(Exit JEdit using the menu)
[1] Done /opt/Isabelle2016/Isabelle2016
% /opt/Isabelle2016/Isabelle2016&
(Isabelle starts normally)
This is on Ubuntu 14.04LTS using Unity.
- Gene Stark
Email Gateway (Aug 22 2022 at 13:51):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Intermittently when starting Isabelle 2016 there is some failure
starting isabelle.jedit.Plugin. I get a popup containing the
following information:
/auto/homes/dpm36/LocalInstalls/Isabelle2016/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start: java.lang.NoClassDefFoundError: scala/Function0
Try updating to a newer version of the plugin.
and printed to the terminal window is the following:
dpm36@pratello:~/Work/Cambridge/github/profuse-formalisation/src$
08:16:00 [main] [error] PluginJAR: Error while starting plugin
isabelle.jedit.Plugin
08:16:00 [main] [error] PluginJAR: java.lang.NoClassDefFoundError:
scala/Function0
08:16:00 [main] [error] PluginJAR: at
java.lang.Class.getDeclaredConstructors0(Native Method)
08:16:00 [main] [error] PluginJAR: at
java.lang.Class.privateGetDeclaredConstructors(Class.java:2671)
08:16:00 [main] [error] PluginJAR: at
java.lang.Class.getConstructor0(Class.java:3075)
08:16:00 [main] [error] PluginJAR: at
java.lang.Class.newInstance(Class.java:412)
08:16:00 [main] [error] PluginJAR: at
org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:933)
08:16:00 [main] [error] PluginJAR: at
org.gjt.sp.jedit.PluginJAR.activatePluginIfNecessary(PluginJAR.java:1021)
08:16:00 [main] [error] PluginJAR: at
org.gjt.sp.jedit.jEdit.main(jEdit.java:549)
08:16:00 [main] [error] PluginJAR: Caused by:
java.lang.ClassNotFoundException: scala.Function0
08:16:00 [main] [error] PluginJAR: at
java.net.URLClassLoader.findClass(URLClassLoader.java:381)
08:16:00 [main] [error] PluginJAR: at
java.lang.ClassLoader.loadClass(ClassLoader.java:424)
08:16:00 [main] [error] PluginJAR: at
sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:331)
08:16:00 [main] [error] PluginJAR: at
java.lang.ClassLoader.loadClass(ClassLoader.java:357)
08:16:00 [main] [error] PluginJAR: at
org.gjt.sp.jedit.JARClassLoader.loadFromParent(JARClassLoader.java:518)
08:16:00 [main] [error] PluginJAR: at
org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:87)
08:16:00 [main] [error] PluginJAR: at
java.lang.ClassLoader.loadClass(ClassLoader.java:357)
08:16:00 [main] [error] PluginJAR: ... 7 more
08:16:00 [main] [error] ErrorListDialog$ErrorEntry:
/auto/homes/dpm36/LocalInstalls/Isabelle2016/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
08:16:00 [main] [error] ErrorListDialog$ErrorEntry: Cannot start:
java.lang.NoClassDefFoundError: scala/Function0
08:16:00 [main] [error] ErrorListDialog$ErrorEntry: Try updating to a
newer version of the plugin.
08:16:00 [main] [error] View: No docking framework PIDE available,
using the original one
08:16:01 [AWT-EventQueue-0] [error] DockableWindowManagerImpl: Unknown
dockable window: isabelle-output
08:16:01 [AWT-EventQueue-0] [error] DockableWindowManagerImpl: Unknown
dockable window: isabelle-theories
Strangely, after quitting and restarting Isabelle/jEdit after seeing
this error, all mathematical symbols in the file I was originally
trying to open when the error occurred are no longer rendered.
Further, there seems to be no way to get any symbols back in a file
without copying and pasting the original contents into a completely
new file (i.e. when typing \rightharpoonup, the usual symbol popup box
appears, but there are no symbols contained within the box rather only
their textual codes, and selecting \rightharpoonup from the popup
simply places the text \rightharpoonup into my theory file, not a
harpoon symbol).
What is happening to an Isabelle .thy file when the failure above
occurs to cause symbols to stop rendering, and how do I fix a file to
get all my symbols back without needing to keep copying-and-pasting
text into fresh files?
Thanks for any help,
Dominic
Email Gateway (Aug 22 2022 at 13:51):From: Lars Hupel <hupel@in.tum.de>
Hi Dominic,
while I don't know the exact cause of the symptoms you're describing, it
sounds like you have a bad Isabelle installation.
/auto/homes/dpm36/LocalInstalls/Isabelle2016/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start: java.lang.NoClassDefFoundError: scala/Function0
Try updating to a newer version of the plugin.
This is the absence of a definition from the Scala library. This could
either mean that the JAR file is corrupted or missing. By chance, are
you running this from an NFS?
What is happening to an Isabelle .thy file when the failure above
occurs to cause symbols to stop rendering, and how do I fix a file to
get all my symbols back without needing to keep copying-and-pasting
text into fresh files?
This usually happens when one copy-pastes something from outside into
Isabelle/jEdit. For me it works after pressing F5 to reload the file.
But the absence of rendering definitely should not happen when you load
a file into the editor.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:51):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Lars,
Thanks for the reply. I'm running Isabelle on my university machine,
which I believe means that I'm running Isabelle over an NFS, yes.
Thanks,
Dominic
Email Gateway (Aug 22 2022 at 13:51):From: Makarius <makarius@sketis.net>
On 25/07/16 09:35, Dominic Mulligan via Cl-isabelle-users wrote:
Intermittently when starting Isabelle 2016 there is some failure
starting isabelle.jedit.Plugin. I get a popup containing the
following information:/auto/homes/dpm36/LocalInstalls/Isabelle2016/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start: java.lang.NoClassDefFoundError: scala/Function0
Try updating to a newer version of the plugin.
Does "intermittently" mean that the failure happens every time you start
Isabelle/jEdit, or only sometimes?
Technically, it means that the JVM cannot access certain jars, notably
the ones of Scala itself. Without that, Isabelle does not work at all.
Strangely, after quitting and restarting Isabelle/jEdit after seeing
this error, all mathematical symbols in the file I was originally
trying to open when the error occurred are no longer rendered.
You need to make sure that files are loaded with the encoding
UTF-8-Isabelle (see the menu File / Reload with Encoding).
This encoding is provided by the Isabelle plugin of jEdit, so without
the plugin editor falls back on something else and makes that persistent
for next time.
Makarius
Email Gateway (Aug 22 2022 at 13:52):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Makarius,
Does "intermittently" mean that the failure happens every time you start
Isabelle/jEdit, or only sometimes?
I'd estimate one in every twenty Isabelle starts suffers from this
problem on my machine. So, not every time I start Isabelle, but often
enough for it to start becoming a pain. Further, I have also
witnessed this same problem on another machine, when Isabelle was
started inside a Docker container.
You need to make sure that files are loaded with the encoding
UTF-8-Isabelle (see the menu File / Reload with Encoding).This encoding is provided by the Isabelle plugin of jEdit, so without
the plugin editor falls back on something else and makes that persistent
for next time.
Thanks, this fixed the problem with my file not having symbols replaced.
Thanks,
Dominic
Email Gateway (Aug 22 2022 at 14:00):From: Makarius <makarius@sketis.net>
Thanks. This is sufficient to reproduce the problem, which is actually
rather profane and without esoteric effects of JVM startup or warmup.
The problem is some invalid application state that remains after killing
the JVM. The next startup tries to connect to an already running
applications, but it does not work.
The situation can be improved by replacing Isabelle2016/Isabelle2016.run
with the included version. Note that the file needs to be executable.
This is only relevant to Linux: the Windows and Mac OS X applications
are different.
Makarius
Isabelle2016.run
Last updated: Nov 21 2024 at 12:39 UTC