FAQ

For troubleshooting, run KeYmaera X from the command line with

java -jar keymaerax.jar

First-Time Startup on MacOS

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.

Multiple KeYmaera X Running

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.

Missing/wrong MathKernel

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.

Missing/wrong Mathematica/Wolfram Engine native library configuration

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.

Java Class File Version Mismatch

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.

Mathematica/Wolfram Engine 12.2 and 12.3 on Ubuntu

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

Unsupported getCallerClass

The command line prints a warning

WARNING: sun.reflect.Reflection.getCallerClass is not supported. This will impact performance.

Solution: ignore

Corrupt file

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.

Weird behavior after an update

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.