Bundling Dynamic Libraries Inside JAR for Ease of Redistribution

[efeg]

Currently to use the Java API on Linux platform, the developer must explicitly compile and link the dynamic libraries.

It would be much easier to integrate Z3 to an existing Java project if it could bundle dependencies in just one or multiple JAR files. These JAR file(s) should contain the required dynamic libraries for the specific platform.

[wintersteiger]

We can't distribute fully compiled and linked .jar files for all platforms, but it would indeed be nice if the build system would automatically put everything into one .jar file during compilation. It's been a while since I looked into this, but back then I couldn't find a small-effort solution that would work on all platforms (especially Windows). I'd be happy about suggestions from the Java experts though.

[cheshire]

In our library we use distribute the .SO file separately using Ivy (https://github.com/sosy-lab/java-smt). I think since most Java projects use some kind of build system (Maven/Gradle/ANT+Ivy), this is preferable to bundling binaries inside the JAR.

[wintersteiger]

Thanks for the comment @cheshire, I agree with you too. Some people are thinking about or working on binary packages for various systems which for many users will mean that it's super easy to install libz3.so, and then they can use any API package without worrying about the binaries.

[cheshire]

We currently have Z3 binaries in our internal Ivy. Would it be possible to push it to Maven central?..

[wintersteiger]

I don't know. What's Ivy? In general pulibshing packages is encouraged, as long as the maintainer is actually doing the maintenance. I have no idea about Ivy and the conditions for maintainers in Maven though.

[cheshire]

Java developers seem to have an enterprise world of their own :P

Ivy (https://en.wikipedia.org/wiki/Apache_Ivy) is a write-once repository with binary artifacts, where maintainers put packages with versions and metadata, and users get them from. A possible analogy is a local installation of PyPi.

Maven central is a global repository for Java packages, sort of like PyPi for python. I'm not sure whether they allow binary artifacts in though.

[wintersteiger]

Thanks for the info! Sure, sounds good to me as long as this isn't a one-shot event where a binary is pushed but never updated. You seem to be using it actively though, so I suppose it wouldn't be much of a problem to keep it up to date, right?.

[cheshire]

@wintersteiger Sorry for the late reply. Z3 binaries are already available inside our own Ivy repository (http://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/, configuration specified at https://github.com/sosy-lab/java-smt/blob/master/ivy.xml), which is updated and maintained regularly. AFAIK that can be fetched by Maven, but I am not 100% sure.

After the JavaSMT release we plan to push to Maven central as well, that should happen in about one month. I would intend to maintain the binary up-to-date for about a year, can't give longer guarantees at the moment. If we push to Maven central, how would the path look like? Ideally it should be under Microsoft organization, but that would require maintenance from your part.

[wintersteiger]

I think it should be within it's own "Z3 Theorem Prover" organization, not necessarily under Microsoft (just like it is on GitHub; it's neither in Microsoft nor in Microsoft Research). Alternatively, the name/organization of the maintainer would make sense so that the first point of contact for any problems is the one who knows the system/environment.

Regarding longer term maintenance, a year is absolutely fine, but when it gets close to the end you should propose a new maintainer, otherwise we have to reserve the right to remove the package because we can't support all of them by ourselves.

Also, please be absolutely clear in package name and descriptions, about what is actually being provided. It seems to me that this provides custom, specific to Ivy Java bindings for a native pre-compiled version of Z3 that is not customized to the users system, and, crucially, the package does not provided the default Java bindings. Further, the README instructs the user to clone the unstable branch, which has been removed about a year ago. So, when you push that package to a public repository please do not call it 'z3', instead rather call it `z3-only-for-ivy' or something like that, and for the organization use the same as for Ivy.

[cheshire]

Hi, thanks for the fast response!

That README file is obsolete and should be updated/removed. We distribute the libz3.so file, as seen in the Ivy repository. While we indeed have our own JNI bindings, the .so file is only specific to the architecture under which Z3 was compiled (x86_64) and hopefully nothing else (definitely not Ivy).

I was talking about distributing the .so file, which I think is the more difficult part (for bindings the user can just download the JAR file).

[cheshire]

I'll try to see with maintainers of Maven central whether there are ways to add .so files. So far people were wrapping them inside JARs, but that is suboptimal for both clarity and performance.

[no-preserve-root]

I have created a solution under https://github.com/tudo-aqua/z3-turnkey. What I did in by build script was:

• download Z3 source code + prebuilt libraries
• execute the code generation scripts
• use AST rewriting to replace the Native.java static initializer with a call to my code (this could be done in Z3 by modifying the native glue generator)
• fix the search path for libz3java.dylib to a relative path (this could be done in Z3 using compiler flags)
• pack everything into one big jar.

At runtime, when Native.class is loaded, my code then

• identifies OS + CPU architecture
• unpacks the correct libz3 and libz3java to a temporary directory
• loads them using System.load() instead of System.loadLibrary().

This is fairly similar to what other Java projects with native dependencies do. In principle, this solution could be adapted for Z3. Until then, I intend to maintain it in tandem with Z3 releases.

[espresso-if]

I currently use z3-turnkey and find the solution very elegant. Wouldn't it be possible for z3 to integrate this capability directly into your release, further facilitating access to z3?

Unfortunately z3-turnkey is currently stuck at 4.8.12

Thanks again for your great contributions to smt solvers

[NikolajBjorner]

I didn't know about z3-turnkey. I can see it has what looks like a nice matrix of CI but it has no releases, but I didn't find releases for it and the Action doesn't upload to a registry from what I can tell.

Maven has https://mvnrepository.com/artifact/org.sosy-lab/javasmt-solver-z3 from last year. This is built maybe somewhere else.

Something that uploads in a GitHub Action automatically to a registry would take out installation needs. The approach undertaken for TS https://github.com/Z3Prover/z3/pull/5762 would be great to aspire to: It is a self-contained package that culminates with upload to nmpjs.

Pull requests that achieve an adequate variant for Java are welcome and having the CI/CD pipeline on may ensure the versions are updated in tandem with other code changes.