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.