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!