Ask for suggestions for the next z3 package release

Ecosystem
,
7

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.