java-smt
java-smt copied to clipboard
sosy-lab
Yices2 MacOS Support
This PR extends the compile script for the Yices2j JNI-wrapper to support a Darwin-based system. The wrapper is statically linked with its dependencies to produce the single file libyices2j.dylib.
I tested it on an Apple M2 with Sonoma 14.6.1. The targets were arm64, as well as x86_64 (Rosetta 2, with arch x86_64 ./compile.sh). I compiled with clang. For this test, I built Yices 2.6.4 with ./configure --enable-thread-safety. Dependencies were installed using brew: gmp 6.3.0, gperf 3.1, openjdk@21 21.0.4. The build may deviate from what you use on Linux.
The modifications on compile.sh should not interfere with the Linux build, but this must be tested. I also modified the wrapper code to fix usages from potentially uninitialized variables.
This may conflict with #215.
I would like to use it aswell -- are there any plans to move this forward, or is there any fundamental blocker?
We appreciate your patience and understand the requirement. At the moment, our team lacks deep expertise with macOS and also the corresponding hardware. Getting started on this will likely require additional time and effort. Supporting macOS presents some unique challenges with native libraries, including:
- Testing Constraints: We don’t currently have the setup to test on macOS. While some CI tools support it, we lack the initial configuration and developer machines to make it happen.
- Publishing Hurdles: Signing and publishing native libraries for macOS is complex, requiring an Apple Developer account and macOS-specific tools (only available on macOS). Cross-compilation is also something we’re unsure about here.
We’d love to improve macOS support down the line, but with our current resources, it’s not something we can address quickly. If you have any specific suggestions or details that could help us move this along, please let us know - we’d be happy to collaborate. We’ll keep this issue open to track progress and interest.
Related issues:
- https://github.com/sosy-lab/java-smt/issues/384
- https://github.com/sosy-lab/java-smt/pull/430
