Email Gateway (Feb 20 2024 at 16:10): Email Gateway (Feb 20 2024 at 16:10):From: Peter Hoefner <cl-isabelle-users@lists.cam.ac.uk>
HI all,
I tried to install Linter [1] on my MacBook Pros (Intel and Apple silicon), running MacOS 14.3.
While the terminal command “Isabelle jedit” works without any problems, opening the app “Isabelle 2023” yields an error:
"Cannot start: java.lang.NoClassDefFoundError: isabelle/jedit_linter/Linter_Plugin”
The plugin manager shows Linter, but indicates an error.
Any suggestions on how to solve this issue?
Cheers
Peter
[1] github.com/isabelle-prover/isabelle-linter
Email Gateway (Mar 06 2024 at 05:15):From: Peter Hoefner <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
I still have this problem, but found more detail regarding the error - hopefully some developer can fix this issue.
Here’s how to replicate the error (including error message) on a Mac (Intel or Apple silicon)
a) Install and run Isabelle2023-app
b) when checking jars in ~/.isabelle/Isabelle2023/jedit/jars, I found
isabelle_jedit_base.jar
isabelle_jedit_main.jar
c) Download and install Linter by executing
./isabelle components -u /Applications/isabelle-linter
Added component "/Applications/isabelle-linter"
d) Checking jars in ~/.isabelle/Isabelle2023/jedit/jars again. One new jar appeared
isabelle_jedit_base.jar
isabelle_jedit_main.jar
isabelle_jedit_linter.jar
e) starting “isabelle jedit” work fine
f) starting App or Isabelle2023 behave equivalent, but different to “Isabelle jedit"
“Cannot start: java.lang.NoClassDefFoundError: isabelle/jedit_linter/Linter_Plugin”
More error messages below [1]
g) Since a jar seems to be missing, I copying jar from linter repo into local folder ~/.isabelle/Isabelle2023/jedit/jars
cp /Applications/isabelle-linter/jedit_linter/lib/classes/isabelle_linter_plugin.jar .
h) starting App or Isabelle2023 now leads invocation exception
/Users/peterhofner/.isabelle/Isabelle2023/jedit/jars/isabelle_jedit_linter.jar:
Cannot start: java.lang.reflect.InvocationTargetException
More error messages below [2]
Any help would be appreciated
Cheers
Peter
[1]
./Isabelle2023
[main] [error] PluginJAR: Error while starting plugin isabelle.jedit_linter_plugin.Plugin
[main] [error] PluginJAR: java.lang.NoClassDefFoundError: isabelle/jedit_linter/Linter_Plugin
[main] [error] PluginJAR: at java.base/java.lang.ClassLoader.defineClass1(Native Method)
[main] [error] PluginJAR: at java.base/java.lang.ClassLoader.defineClass(ClassLoader.java:1012)
[main] [error] PluginJAR: at java.base/java.lang.ClassLoader.defineClass(ClassLoader.java:874)
[main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader._loadClass(JARClassLoader.java:436)
[main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:109)
[main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:926)
[main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePluginIfNecessary(PluginJAR.java:1026)
[main] [error] PluginJAR: at org.gjt.sp.jedit.jEdit.main(jEdit.java:530)
[main] [error] PluginJAR: at isabelle.jedit.JEdit_Main$.$anonfun$5(jedit_main.scala:126)
[main] [error] PluginJAR: at isabelle.jedit.JEdit_Main$.main(jedit_main.scala:135)
[main] [error] PluginJAR: at isabelle.jedit.JEdit_Main.main(jedit_main.scala)
[main] [error] PluginJAR: Caused by: java.lang.ClassNotFoundException: isabelle.jedit_linter.Linter_Plugin
[main] [error] PluginJAR: at java.base/jdk.internal.loader.BuiltinClassLoader.loadClass(BuiltinClassLoader.java:641)
[main] [error] PluginJAR: at java.base/jdk.internal.loader.ClassLoaders$AppClassLoader.loadClass(ClassLoaders.java:188)
[main] [error] PluginJAR: at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:520)
[main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadFromParent(JARClassLoader.java:519)
[main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:87)
[main] [error] PluginJAR: at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:520)
[main] [error] PluginJAR: ... 11 more
[main] [error] ErrorListDialog$ErrorEntry: /Users/peterhofner/.isabelle/Isabelle2023/jedit/jars/isabelle_jedit_linter.jar:
[main] [error] ErrorListDialog$ErrorEntry: Cannot start: java.lang.NoClassDefFoundError: isabelle/jedit_linter/Linter_Plugin
[2]
./Isabelle2023
[main] [error] PluginJAR: Error while starting plugin isabelle.jedit_linter_plugin.Plugin
[main] [error] PluginJAR: java.lang.reflect.InvocationTargetException
[main] [error] PluginJAR: at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
[main] [error] PluginJAR: at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:77)
[main] [error] PluginJAR: at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
[main] [error] PluginJAR: at java.base/java.lang.reflect.Constructor.newInstanceWithCaller(Constructor.java:499)
[main] [error] PluginJAR: at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:480)
[main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:938)
[main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePluginIfNecessary(PluginJAR.java:1026)
[main] [error] PluginJAR: at org.gjt.sp.jedit.jEdit.main(jEdit.java:530)
[main] [error] PluginJAR: at isabelle.jedit.JEdit_Main$.$anonfun$5(jedit_main.scala:126)
[main] [error] PluginJAR: at isabelle.jedit.JEdit_Main$.main(jedit_main.scala:135)
[main] [error] PluginJAR: at isabelle.jedit.JEdit_Main.main(jedit_main.scala)
[main] [error] PluginJAR: Caused by: java.lang.ExceptionInInitializerError
[main] [error] PluginJAR: at isabelle.jedit_linter.Linter_Plugin.<init>(linter_plugin.scala:16)
[main] [error] PluginJAR: at isabelle.jedit_linter_plugin.Plugin.<init>(plugin.scala:6)
[main] [error] PluginJAR: ... 11 more
[main] [error] PluginJAR: Caused by: java.lang.IllegalAccessException: module java.base does not open java.lang.reflect to unnamed module @78452606
[main] [error] PluginJAR: at java.base/java.lang.invoke.MethodHandles.privateLookupIn(MethodHandles.java:259)
[main] [error] PluginJAR: at isabelle.jedit_linter.JEdit_Extension$.<clinit>(jedit_extension.scala:22)
[main] [error] PluginJAR: ... 13 more
[main] [error] ErrorListDialog$ErrorEntry: /Users/peterhofner/.isabelle/Isabelle2023/jedit/jars/isabelle_jedit_linter.jar:
[main] [error] ErrorListDialog$ErrorEntry: Cannot start: java.lang.reflect.InvocationTargetException
Email Gateway (Mar 06 2024 at 08:04):From: Fabian Huch <huch@in.tum.de>
Hi Peter,
thank you for you report -- currently, I'm afraid you'll have to start
Isabelle via command-line with 'isabelle jedit' for the linter to work.
Best,
Fabian
Email Gateway (Mar 11 2024 at 00:45):From: Peter Hoefner <cl-isabelle-users@lists.cam.ac.uk>
Thanks for the response Fabian.
Happy to use the command-line option for the time being.
Peter
Balazs Toth (Mar 11 2024 at 08:28):Email Gateway said:
From: Peter Hoefner <cl-isabelle-users@lists.cam.ac.uk>
Thanks for the response Fabian.Happy to use the command-line option for the time being.
Peter
Hi Peter,
I used this approach as a workaround to still have a shortcut: https://stackoverflow.com/questions/46397647/how-to-create-dock-icon-for-running-terminal-command-in-mac-os
Best,
Balazs
Last updated: Apr 29 2024 at 04:18 UTC