Email Gateway (Aug 22 2022 at 16:21): Email Gateway (Aug 22 2022 at 16:21):From: David Schneider <david.f.schneider@gmail.com>
I am having trouble installing Isabelle on Mac OS X (10.12). (It has been a
few years since I last actually installed Isabelle.) I have tried Isabelle
2015, 2016-1, and 2017, all with no success. Upon starting the application,
Isabelle appears briefly in the dock and then just closes again.
I am suspecting that this has something to do with the remark "Note that
the target directory needs to be writable when Isabelle is started for the
first time, to build the required logic image" in the installation guide,
but it is not clear to me what exactly this directory is.
Any help is greatly appreciated.
Best,
David
Email Gateway (Aug 22 2022 at 16:21):From: Makarius <makarius@sketis.net>
That is only relevant for the Isabelle session build process, when the
main application is already running.
I guess this new note from our "Installation" page id relevant:
Note: The Isabelle application lacks special certificates and
signatures, so Apple tends to reject it by default. Running it for the
first time might require a right-click or control-click on the
application icon to open it explicitly.
Makarius
Email Gateway (Aug 22 2022 at 16:21):From: David Schneider <david.f.schneider@gmail.com>
I've put the bundle into the Applications folder as described in the
installation notes. Hence, this directory should be writable.
I am also not getting any notification that execution was blocked due the
developer being unverified.
As a little experiment, I tried starting the build process on the terminal
by calling ./bin/isabelle build -a. Interestingly, when doing this, I am
getting errors that Scala methods are missing. For Isabelle2016-1, this is
Exception in thread "main" java.lang.NoSuchMethodError:
scala.Predef$.ArrowAssoc(Ljava/lang/Object;)Ljava/lang/Object;
For Isabelle2017, this is
Exception in thread "main" java.lang.NoSuchMethodError:
scala.Product.$init$(Lscala/Product;)V
I am not sure whether this is the actual problem or whether this just
happens because the build process is not supposed to be called in this way.
This looks like I might be running with an old version of the Scala
libraries on the class path. However, I am not aware of any other Scala
installation on my machine (after having looked thoroughly).
Best,
David
Email Gateway (Aug 22 2022 at 16:21):From: Makarius <makarius@sketis.net>
It should be definitely possible to run the Isabelle command-line tools
via bin/isabelle from the app directory. In particular, it often makes
sense to run something like "Isabelle2017.app/Isabelle/bin/isabelle
jedit" with special options.
The above class loader errors indicate a more fundamental problem. Here
are some guesses from a distance:
* The download somehow went wrong and the jars are broken.
* The target file-system is somehow odd, e.g. with encryption options
that Java and/or Scala don't like.
* Your process environment (e.g. .bashrc) provides JAVA_HOME and/or
SCALA_HOME that is incompatible with the Java and Scala included in the
Isabelle app. You can also try "bin/isabelle getenv JAVA_HOME" or the
same with SCALA_HOME to investigate this.
Makarius
Email Gateway (Aug 22 2022 at 16:24):From: David Schneider <david.f.schneider@gmail.com>
I finally got around to investigating this further. However, I am
unfortunately still at a loss.
2017-11-06 21:57 GMT+01:00 Makarius <makarius@sketis.net>:
On 06/11/17 20:02, David Schneider wrote:
As a little experiment, I tried starting the build process on the
terminal by calling ./bin/isabelle build -a. Interestingly, when doing
this, I am getting errors that Scala methods are missing. For
Isabelle2016-1, this is
Exception in thread "main" java.lang.NoSuchMethodError:
scala.Predef$.ArrowAssoc(Ljava/lang/Object;)Ljava/lang/Object;For Isabelle2017, this is
Exception in thread "main" java.lang.NoSuchMethodError:
scala.Product.$init$(Lscala/Product;)VI am not sure whether this is the actual problem or whether this just
happens because the build process is not supposed to be called in this
way. This looks like I might be running with an old version of the Scala
libraries on the class path. However, I am not aware of any other Scala
installation on my machine (after having looked thoroughly).It should be definitely possible to run the Isabelle command-line tools
via bin/isabelle from the app directory. In particular, it often makes
sense to run something like "Isabelle2017.app/Isabelle/bin/isabelle
jedit" with special options.
I tried this out, but it also leads to the following error, which is
similar to those I encountered when running isabelle build:
David:Isabelle2017.app david$ ./Isabelle/bin/isabelle jedit
Exception in thread "main" java.lang.NoSuchMethodError:
scala.Predef$.augmentString(Ljava/lang/String;)Ljava/lang/String;
at isabelle.GUI$.<init>(gui.scala:127)
at isabelle.GUI$.<clinit>(gui.scala)
at isabelle.Main$.main(main.scala:110)
at isabelle.Main.main(main.scala)
The above class loader errors indicate a more fundamental problem. Here
are some guesses from a distance:* The download somehow went wrong and the jars are broken.
Since I tried downloading the versions of Isabelle multiple times, both
times with no indications of any problems and both times giving the same
results, I think I can rule out this possibility.
* The target file-system is somehow odd, e.g. with encryption options
that Java and/or Scala don't like.
I am using the standard APFS file system. In particular, I am not using
FileVault encryption. I also tried running Isabelle from external drives
using HFS+ and FAT, both times with the same result. Hence, I think I can
also conclude that this is not a problem of the file system.
* Your process environment (e.g. .bashrc) provides JAVA_HOME and/or
SCALA_HOME that is incompatible with the Java and Scala included in the
Isabelle app. You can also try "bin/isabelle getenv JAVA_HOME" or the
same with SCALA_HOME to investigate this.
Everything seems to be in order here as well. For Isabelle 2017, I get the
following results:
David:Isabelle2017.app david$ ./Isabelle/bin/isabelle getenv JAVA_HOME
JAVA_HOME=/Applications/Isabelle2017.app/Contents/Resources/Isabelle2017/contrib/jdk/x86_64-darwin/Contents/Home/jre
David:Isabelle2017.app david$ ./Isabelle/bin/isabelle getenv SCALA_HOME
SCALA_HOME=/Applications/Isabelle2017.app/Contents/Resources/Isabelle2017/contrib/scala-2.12.3
Makarius
In conclusion, I am still none the wiser what the problem actually is. This
is most frustrating. I'd be very grateful for any further ideas.
Best,
David
Email Gateway (Aug 22 2022 at 16:24):From: Makarius <makarius@sketis.net>
On 15/11/17 16:16, David Schneider wrote:
I finally got around to investigating this further. However, I am
unfortunately still at a loss.Everything seems to be in order here as well. For Isabelle 2017, I get
the following results:David:Isabelle2017.app david$ ./Isabelle/bin/isabelle getenv JAVA_HOME
JAVA_HOME=/Applications/Isabelle2017.app/Contents/Resources/Isabelle2017/contrib/jdk/x86_64-darwin/Contents/Home/jre
David:Isabelle2017.app david$ ./Isabelle/bin/isabelle getenv SCALA_HOME
SCALA_HOME=/Applications/Isabelle2017.app/Contents/Resources/Isabelle2017/contrib/scala-2.12.3
Both of this looks OK.
In conclusion, I am still none the wiser what the problem actually is.
This is most frustrating. I'd be very grateful for any further ideas.
Yet another idea: instead of using the official application bundle, run
everything from the repository. See the section "Quick start in 30min"
in
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/README_REPOSITORY
If you use "hg clone -r Isabelle2017" or after the clone "hg up -r
Isabelle2017", you get exactly to the official release with its add-on
components. Otherwise you get an arbitrary version in the middle of
nowhere between releases.
The remaining command sequence from README_REPOSITORY should all work,
although there can be confusion of command-line tools in rare cases
(official ones by Apple vs. other ones from MacPorts, Homebrew etc.).
Makarius
Email Gateway (Aug 22 2022 at 16:24):From: David Schneider <david.f.schneider@gmail.com>
I tried this out and ran the following:
hg clone http://isabelle.in.tum.de/repos/isabelle -r Isabelle2017
cd isabelle
./bin/isabelle components -I
./bin/isabelle components -a
./bin/isabelle jedit -l HOL
No luck, unfortunately. After building Isabelle/Scala and Isabelle/jEdit,
this leads to the same error as before:
Exception in thread "main" java.lang.NoSuchMethodError:
scala.Predef$.augmentString(Ljava/lang/String;)Ljava/lang/String;
at isabelle.GUI$.<init>(gui.scala:127)
at isabelle.GUI$.<clinit>(gui.scala)
at isabelle.Main$.main(main.scala:110)
at isabelle.Main.main(main.scala)
The paths are now the following:
SCALA_HOME=/Users/david/.isabelle/contrib/scala-2.12.3
JAVA_HOME=/Users/david/.isabelle/contrib/jdk-8u144/
x86_64-darwin/Contents/Home/jre
Best,
David
Email Gateway (Aug 22 2022 at 16:25):From: Makarius <makarius@sketis.net>
Can you show me the result of this:
./bin/isabelle getenv CLASSPATH ISABELLE_CLASSPATH
Makarius
Email Gateway (Aug 22 2022 at 16:26):From: David Schneider <david.f.schneider@gmail.com>
I was able to fix the problem now: In the process of trying to install the
right version of Scala on my machine, I found that SBT did not run either.
Googling that particular error message pointed me to the fact that I had an
ancient version of the Scala library (from 2012) in the Java extension
directory (/Library/Java/Extensions). After removing this library, Isabelle
now runs perfectly fine. Apparently, the last version of Isabelle I
installed on the machine in question did not use Scala yet, which is why I
did not encounter this problem before.
Thanks a lot for the help!
Best,
David
Last updated: Apr 26 2024 at 16:20 UTC