Ask for suggestions for the next z3 package release

,

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