search

LS-Lab / KeYmaeraX-release

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
http://keymaeraX.org/
GNU General Public License v2.0
76 stars 38 forks source link

Backend Tool Termination - undefined symbol: uuid_generate #72

Closed Bckempa closed 3 years ago

Bckempa commented 3 years ago

When configuring either Mathmatica or Wolfram Engine, KeYmaeraX terminates with a symbol lookup error.

OS: Ubuntu 20.04 (Linux 5.8.0-41) JRE: Tested with OpenJDK 8, 11, 13, 14 and Oracle Java 11 KeYmaeraX: 4.9.3 Mathematica & Wolfram Engine: 12.2

Error: {PATH_TO_JVM}: symbol lookup error: {PATH_TO_JLINK}: undefined symbol: uuid_generate

Reproduction: From fresh KeYmaeraX install, configure path to J/Link library for either Mathematica 12.2 or Wolfram Engine 12.2. KeYmaeraX will immediately terminate with error and terminate after restarting until JLINK_LIB_DIR keys are removed from .conf

Bckempa commented 3 years ago

Confirmed to work as expected after installing Mathematica 12.1 with no other changes. Appears to be an incompatibility with the latest Wolfram point release.

smitsch commented 3 years ago

Fixed in f3ef3c7bfa3f0a6047b4d772e70ea4c54d3dfee2

nrfulton commented 3 years ago

I get the same error when using WolframEngine 12.3.

smitsch commented 3 years ago

The incompatibility seems to be inside the JLink native code library and present since 12.2. We filed a bug report with Wolfram.

smitsch commented 3 years ago

I found a workaround.

Locate libuuid.so using find / -type f -iname "libuuid*", 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

nrfulton commented 3 years ago

Thank! Is this me worth incorporating into the startup sequence (eg where we also do the memory limits and such), or are we fairly confident Mathematica will push a fix soon?

smitsch commented 3 years ago

Wolfram support assured me that they forwarded the report to development, but didn't give an ETA. Might be worth including in the startup sequence for now.