-
Notifications
You must be signed in to change notification settings - Fork 39
Running KeYmaera X
For troubleshooting, run KeYmaera X from the command line with
java -jar keymaerax.jar
On MacOS, the error
"keymaerax.jar" cannot be opened because it is from an unidentified developer
indicates that you have to use the Right-click→Open menu the first time you start keymaerax.jar and/or allow starting it in the security settings.
The command line warning
[launcher] WARNING: A lock file exists but nothing is bound to the KeYmaera X web server's port.
Deleting the lock file and starting KeYmaera X. If you experience errors, try killing all
instances of KeYmaera X from your system's task manager.
indicates that KeYmaera X might be running or did not shut down correctly.
Solution: Shut down other KeYmaera X instances before starting a new one. If none is running, delete the file ~/.keymaerax/lockfile (on Windows: C:\Users\[You]\.keymaerax\lockfile) and try starting again.
KeYmaera X displays
Warning: Limited functionality: Neither Mathematica nor Wolfram Engine is configured
Effect: Mathematica is not available, KeYmaera X will use Z3 instead and work with limited functionality.
Solution: Open the KeYmaera X preferences and enter/fix the path (default paths give hints where to search), or edit the configuration file ~/.keymaerax/keymaerax.conf (on Windows: C:\Users\[You]\.keymaerax\keymaerax.conf) to fix the entry MATHEMATICA_LINK_NAME or WOLFRAMENGINE_LINK_NAME.
The command line prints an error
Fatal error: cannot find the required native library named JLinkNativeLibrary.
Effect: Mathematica is not available, KeYmaera X will use Z3 instead and work with limited functionality.
Solution: Search the file libJLinkNativeLibrary.jnilib (MacOS, inside the /Applications/Mathematica.app package), libJLinkNativeLibrary.so (Linux), or JLinkNativeLibrary.dll (Windows). Open the KeYmaera X preferences and enter the path without file name, or edit the configuration file ~/.keymaerax/keymaerax.conf (on Windows: C:\Users\[You]\.keymaerax\keymaerax.conf) to fix the entry MATHEMATICA_JLINK_LIB_DIR or WOLFRAMENGINE_JLINK_LIB_DIR.
The command line prints an error
Exception in thread "main" java.lang.UnsupportedClassVersionError: ... has been
compiled by a more recent version of the Java Runtime (class file version X),
this version of the Java Runtime only recognizes class file versions up to Y
Solution: KeYmaera X needs at least Java 11. Install Java 11 or newer and double-check with java -version that Java 11 is used for running from the command line.
The command line prints an error
{PATH_TO_JVM}: symbol lookup error: {PATH_TO_JLINK}: undefined symbol: uuid_generate
Solution: locate libuuid.so using find / -type f -iname "libuuid*", located for example in /lib/x86_64-linux-gnu/libuuid.so.1.3.0.
Then start KeYmaera X as follows: export LD_PRELOAD=/lib/x86_64-linux-gnu/libuuid.so.1.3.0;java -jar keymaerax.jar
The command line prints a warning
WARNING: sun.reflect.Reflection.getCallerClass is not supported. This will impact performance.
Solution: ignore
The command line prints an error
Invalid or corrupt jarfile
Solution: KeYmaera X needs at least Java 11. Install Java 11 or newer and double-check with java -version that Java 11 is used for running from the command line.
Solution: clean your local cache by removing the directory ~/.keymaerax/cache. You can also rename the model and proof database ~/.keymaerax/keymaerax.sqlite.
It is good practice to periodically export KeYmaera X proof archives to separate files.