Ask for suggestions for the next z3 package release

,

We are preparing for the new release for the OCaml binding for z3 4.8.13 after fixing the linking problem on macOS.

We have some discussion in the PR to the opam repo on how the package should be. Let me recap our tentative choice with some background. We would like to post it here instead of just chatting between us inside the issue.

Our tentative choices
TC1: Opam package z3 4.8.13 will use the shared library libz3.so(libz3.dylib) of z3 on linux and macos.
TC2: No opam package for z3 static binding for 4.8.13.

The status of z3 bindings, current and before
In our testing, the OCaml binding using the z3 shared library (z3-shared for short) works correctly on both platforms.
The OCaml binding using the z3 static library (z3-static) works fine only on linux, but has fatal bugs C++ ABI mismatch on macOS when using some z3 API. The above links contain all the details.
Looking back, z3 package changes the binding type of z3 (shared: before 4.8.1; static: 4.8.4 - 4.8.12) due to some bugs before.

We had a hard discussion in the PR on how we shall handle the partial-working z3-static. For mac users like @k4rtik or me, we don’t care using which binding as long as it works. @MSoegtropIMC shares the experience of maintaining Coq Platform that I want to copy here:

To get forward let me explain why I am against a split. The main issue I see is that the two packages won’t be compatible, because they will partly install the same file (I guess the z3 executable e.g.). People not on MacOS will likely randomly choose one or the other package for z3. This way we will quickly end up with a situation where people create packages which are not compatible with macOS. Worse is that we will have packages which cannot be installed together, because one uses the static and one the non static version, and these can’t be installed together. I maintain a largish opam meta project (Coq Platform) and I have a lot of work with such issues. People think they make things flexible by offering variants, but by this they in the end reduce flexibility cause they introduce unnecessary incompatibility points.

Though z3-share and z3-static are in fact compatible in linux (they can be both installed and working), I agree with this argument to withhold the static one.

I am a bit concerning neither @MSoegtropIMC (the largish platform maintainer) nor me (working is everything) can cover all users. So, there is this post.

Best practice to distribute on opam

the critical question I am interested the most is what is the best practice to distribute a package, exactly, an OCaml binding for a C++ library. I reuse most of the previous code to make the binding for simplicity.

Q1: Will using virtual package conf-z3 with opam depext -i to install z3 library better than building z3 in the binding library?

Q2: (Assume we may fix the z3-static on macos later in the future), will it be better to provide both bindings with the shared libraries and static libraries? I know the llvm binding uses the findlib predicate but no more experience on this.

Q3: If Q2 is yes, what is the best way to arrange the shared libraries and static packages?

Q4: If Q2 is no, what is the rescue way if one really wants to use the other binding?

Personally, I would like to have a working (a.k.a. using the shared library) release of z3 on opam quickly. I can make a better version later after the community gives me guidance for the improvement. My another concern is Z3 maintains two building systems: cmake for everything-but-ocaml-binding and a legacy-python-script for our ocaml binding. Nikolaj said it here.

We are appreciating for all the comments regarding each part of the post (tentative choices, best practice, bug fixing).

Thanks in advance!

7 Likes

Hello and thank you for your work on packaging Z3 for OCaml.

I am not familiar with the details of opam packaging, especially when macOS is concerned. However I can speak as an OCaml user of Z3.

Q1: Will using virtual package conf-z3 with opam depext -i to install z3 library better than building z3 in the binding library?

Aren’t conf-* packages proxy for system packages? I think a conf-z3 package should find the configuration of an externally installed Z3 (flags, paths, etc), without any control over the version. It is not expected to build a complete distribution of Z3.

I see two potential encodings to work around the issues.

Extra indirection:

  • packages z3-shared and z3-static that build the z3 library in a proper way, with constraints on the systems on which they are available
  • z3 as a “virtual package” to select one of the implementation (favoring z3-shared by default)

Software that requires Z3 should depend solely on the z3 package. End-users are free to choose z3-static explicitly (doing so would recompile z3 and other reverse dependencies if necessary, ensuring consistency).

Optional dependencies to select the configuration:

The main package would be z3. It builds the shared library by default, and has an optional (but not recommended) dependency on z3-static (conf-z3-static?) that marks the desire to get a static version.
z3-static is only available on operating systems for which it is guaranteed to work.

This does not address the case where one wants to have both z3-shared and z3-static in the same switch… This seems to be an edge case that is not worth spending too much time on, at least before one comes up with a compelling use case. This is quite similar to the dune “virtual libraries”, where one can choose two implementations for a single interface at build time (Z3 ML API could even be exposed using this feature, with an external script to handle the C++ build steps).

Q2: (Assume we may fix the z3-static on macos later in the future), will it be better to provide both bindings with the shared libraries and static libraries? I know the llvm binding uses the findlib predicate but no more experience on this.

(Speaking as a Linux user). The slowest part (by far) of my compile cycle is the static linking of Z3.
As a workaround, I use bytecode targets during development (the heavy lifting is done by Z3 anyway, so I don’t lose much by compiling OCaml to bytecode). If I was offered the choice, I would prefer to use z3-shared as much as possible.

I don’t see much value in the static bindings, except maybe for distributing binaries. In that case, using a different switch in which z3-static is explicitly installed might be the best option for ensuring consistent builds. I already use different switches to test different Z3 versions (important for troubleshooting).

Shameless plug: I am developing a Z3 helper library (ZTL). It is far from being released, but when the time comes, I would really like to simply depend on z3 rather than z3-shared. Since this is an intermediate library that will be linked into other projects, it should not impose restrictions or complicate the build and it is very important to avoid the issues mentioned by @MSoegtropIMC.

I don’t know much about cmake, but I am open for discussions and might provide help on the OCaml (including FFI) side of things.

3 Likes

I’m the author of z3overlay and I use Z3 for a bunch of prototypes. I echo all of @let-def’s point: Make a main z3 package that contains only the ocaml bits and depends either on conf-z3 or conf-z3-static (where the non-ocaml stuff come from, either shared or statically linked). Everyone should only ever depend on the z3 package.

The shared version would make day-to-day dev much nicer (z3’s compilation time overshadows everything else when I need to update my switch) and significantly accelerate CI, and the statically-linked version is very useful in other setups.

Regarding build systems: Last time I had to solve related issues, it was actually much easier to build the ocaml bindings by yanking all the files out, slaping a tiny dune file and building it like that, than trying to wrestle the legacy scripts in Z3’s sources. Just a though …

5 Likes

I’m the maintainer* of the llvm library in opam. We’ve faced/facing similar issues:

  • Back in the days (before 3.9) the entire LLVM library along with the OCaml binding was installed. This took ages to compile, used the slow to link static library and overall wasn’t too good of an experience.
  • For the release of LLVM 3.9 I decided to split the package into:
    • conf-llvm: in charge of installing the depexts and gather information about what is installed
    • llvm: that uses these information to compile only the llvm bindings (using the dynamic library)
  • For the release of LLVM 4.0.0, users were missing the option to link LLVM statically so I patched the META file with a “hack” using ocamlfind predicate system for users to be able to select the linking method they wanted.

It pretty much stayed the same since (as a series of scripts and patches only in opam) as I didn’t have much time or motivation and the upstreaming process was long and difficult to keep my attention on.

Last year I started experimenting on another solution: GitHub - kit-ty-kate/llvm-dune: The official LLVM OCaml binding but built using dune
It is an experimental repository vendoring LLVM, with a simple script to make it able to compile llvm using dune (making it faster and easier to maintain) and making use of its (virtual_modules ...) feature to choose between dynamic and static linking. It works fine as-is, however the biggest hurdle and why it hasn’t become the new llvm package yet (aside from my lack of time to dedicate to it) is that it is not compatible with the old ocamlfind “hack” and would change the behaviour silently and I haven’t found the solution to make it compatible yet.

For z3, I think the solution is to go the llvm-dune route in my opinion, it should be much easier for you to go this route now as you don’t have the same compatibilities issues.

*: at least when I have the time or motivation to work on it, which I only get a few times a year…

3 Likes

The OCaml API relies on Z3’s C API, so in theory it could be yanked outside of Z3 and be maintained independently, I suppose? Maybe that’s a reasonable suggestion to make to Nikolaj and the other Z3 maintainers, they might be happy to get rid of in-tree OCaml bindings. In particular, OCaml bindings are the last roadblock in Z3’s full migration to cmake as a build system as they still rely on the magic python build script.

Then the question is: how do the bindings track the evolution of Z3’s API? Currently they don’t really follow recent changes (a lot of things are not exported to OCaml), but if OCaml bindings were to live out-of-tree then there would at least need to be a mechanism to detect that libz3.so is not too old.

4 Likes

I always wanted to remove z3 from the OCaml z3 package the way @c-cube suggested, just never had time for this, so I totally support this initiative and will be happy to help!

The “right to do thing” is to have the conf-z3 package that detects the presence of the system installation of libz3, e.g., libz3-dev The package may set the flags, which will help the downstream packages to determine whether static libraries are present or not and what linker and compilation flags should be passed. It is a quite common situation when the same library have static libraries on one distribution and do not have on the other, so ideally the downstream packages shall try to support either case. This is how we deal with llvm on bap side, if there are static libraries, then we build a statically linked llvm plugin, if the are absent, then we do what we can and have the dependency on the shared library encoded in the plugin.

The problem why I wasn’t able to create a z3 package (and we’re packaging z3 for more than 10 years, in CMU, since the times when it wasn’t even open-source) is that not everything is available in the installed version of the library and the generation of the binding is deeply embedded into the source code of z3. But if we will be able to persuade Nikolaj to extract the z3 ocaml bindings into a separate project then not only we will help with the hygiene of z3, but we will also resolve a lot of problems that we have just because we do not own the bindings. Like the first step that I would make is to eradicate the build system of the bindings and just use dune. Then we will not have all that questions like what to build and what to install and how and where, this will be all handled by dune.

3 Likes

Thanks for your replies.

Split of the package z3

From the replies, I see all of you agree

  1. move z3 libraries out of ocaml z3 package.

  2. use conf-z3 to detect the system installation of libz3.

  3. use the shared library by default.

  4. make the static optional.

The subtle problem now is in the current z3 C++ building. It doesn’t support building the ocaml binding from the already-built z3 libraries within the current python script. Unlike the building of llvm binding, when the source is needed but the llvm libraries are provided from conf-llvm. It’s not a difficult thing but it takes time to finish.

Another problem is the system installation of the latest z3 is more challenging especially on ubuntu. On macos, the system package manager homebrew tracks the latest version quite well (I guess it tracks the github link). I can have z3 4.8.13 installed to satisfy conf-z3. I don’t know an easy way to have package z3 4.8.13 installed on ubuntu via apt or dpkg. I can build and install this z3 from the source but I don’t think this is good. The whole binding is harder to install than before without solving this.

@let-def mentions an externally installed Z3 (flags, paths, etc), without any control over the version.

I can understand this for tools e.g. conf-python-3 or conf-gcc which the exact version is not important. As for the library bindings, I guess there may be more breaking changes e.g. adding a new API. With this split schema, explicit version matching makes the binding safer to use. z3 4.8.14 depends conf-z3 4.8.14 looks more natural to me.

On-the-tree or off-the-tree

This question is in my mind but I deleted it in my original post. I planed to have another post on this later after more observations. In fact, I asked this question in this post and @jjb shares his thought and also mentions @kit-ty-kate 's llvm-dune project.

Besides with the tracking problem @c-cube and @ivg mention, I also wonder the tool to automatic generate the ocaml binding/stublibs from the C API. Z3’s ocaml binding has z3native.ml.pre and z3native_stubs.c.pre (I don’t know yet how they are used to generate the corresponding files yet). I also found @thierry-martinez clangml has a stubgen tool but I don’t know if any general tool for this.

I added a few lines in the z3’s python script and CI to test the post-install of the ocaml binding. I admit it makes Nikolaj a bit more painful to update the C API. The pain should be much reduced if the binding is easier to make.

Other z3 bindings

I have a thin z3 wrapper in my project due to the official API is verbose to use heavily and I use z3.datatype a lot. It’s nice to know ztl and z3overlay and I will read them in detail later.

The bindings contain a Version module (see this for example) so in theory, out-of-tree OCaml bindings could begin by checking just that part, and selecting what bindings to use depending on the version. Some newer features would be gated on major,minor >= 4.8.7 or something like that.

Depending on an exact version of Z3 seems difficult because different distributions will naturally ship with different versions of Z3.

By the way, since z3 migrated for most of the parts to CMake, it would be nice if someone is brave enough to port also the OCaml bindings to it as well, instead of a bunch of unwieldy Python scripts:

I can try porting the ocaml binding to z3 cmake in my next long free time (the winter holiday).

2 Likes

I am happy to see the discussion here and the long-term plan to port the OCaml bindings to CMake.

But in the short-term, is anyone against switching to dynamic binding as in the PR Add Z3 4.8.13 with dynamic loading of libraries by k4rtik · Pull Request #20065 · ocaml/opam-repository · GitHub?

Currently, without this change, Z3 OCaml is broken on several macOS versions.