search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65 stars 20 forks source link

Install error messages on macOS: unable to locate a Java runtime #73

Closed ahelwer closed 1 year ago

ahelwer commented 1 year ago

Here is the output when I try to install https://tla.msr-inria.inria.fr/tlaps/dist/1.4.5/tlaps-1.4.5-i386-darwin-inst.bin on macOS:

ahelwer@ah-mbair Examples % ./tlaps-1.4.5-i386-darwin-inst.bin -d tlaps
Installing the TLA+ Proof System

    Version: 1.4.5
Destination: /Users/ahelwer/Source/tlaplus/Examples/tlaps

Extracting ... done.
Compiling Isabelle theories.
The operation couldn’t be completed. Unable to locate a Java Runtime.
Please visit http://www.java.com for information on installing Java.

Building Pure ...
Finished Pure (0:00:08 elapsed time, 0:00:06 cpu time, factor 0.75)
The operation couldn’t be completed. Unable to locate a Java Runtime.
Please visit http://www.java.com for information on installing Java.

Building TLA+ ...
Finished TLA+ (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.44)
Finished compiling Isabelle theories.
Performing a self-test ... done.

All done.

I installed Java with homebrew, so which java outputs:

/opt/homebrew/opt/openjdk/bin/java

Did the install succeed? If not, what environment variable do I need to set so the installer can find the java installation?

lemmy commented 1 year ago

IIRC the JVM has to be found under /Library/Java/JavaVirtualMachines/:

sudo ln -sfn /opt/homebrew/opt/openjdk/libexec/openjdk.jdk /Library/Java/JavaVirtualMachines/openjdk.jdk
ahelwer commented 1 year ago

Unfortunately I believe the macOS system integrity protection feature keeps you from doing that.

ahelwer commented 1 year ago

Perhaps not, according to https://support.apple.com/en-us/HT204899 the /Library directory is okay; I will try that.

ahelwer commented 1 year ago

Okay that did seem to work. I don't know whether this closes the issue, or perhaps it will just be superseded because 1.4.5 is a bit old now.

muenchnerkindl commented 1 year ago

Great if that worked. The Isabelle error message about not finding a Java runtime can be ignored, the prover works without Java. Also, as you say, the distribution is old and the version of Isabelle that it relies on is ancient. I ported the theories to the current Isabelle version, and I believe that the issue will disappear.