Hi Kakadu and the community,
I have been working on several PRs to improve the `ocaml-z3` by migrating its build system to CMake. Here is some update:
- I migrated building z3’s OCaml binding from a legacy python generated script to CMake (z3#7254, z3#7258). This is **merged**. I added some sanity checks including CMake targets which can be triggered inside of building z3 from the source, as well as Github Actions CI check in the z3-source. It covers `{Linux, MacOS} * {bytecode, native}.`
- I have an unpublished opam `z3.dev` package on my own opam-repository fork, which fetches the latest z3 source and builds it with CMake. I also made a CI there. It checks the installing `z3` package from opam. I use it for a while, and I guess it should be safe to publish.
**On using system-wide z3**, it’s my next serious plan. However, it’s a bit tricky. The current _slow_ approach, that each opam package builds its own z3, can guarantee the z3 version is compatible with the ocaml-z3 bindings. If we want to use the system-wide libz3, say debian’s apt, it usually uses a stable libz3 version, which may be incompatible with opam’s z3 bindings. Also, if we have multiple package z3 in separate opam switches, which cannot share the same system-wide z3, how to guarantee they can work as they used to be? These is one other subtle problem on CMake build/install discussed z3#7684. I notice the Dune team has support package management, and it looks very promising. I will explore it in detail later.
For merely changing the opam z3 package to use CMake instead of the legacy python script, it’s ready to submit. Many of the PRs are done before and in the summer. I was busy in recent weeks due to moving and other DDLs, but I will be free soon. I have some ideas to solve this, and I will try it soon. The opam z3 package can be configured to use the system-wide or standalone as they used to be.
To say a bit more, I call it _serious plan_ because after spending dozens (hundreds?!) of hours on solving this kind of problem and gaining enough experience, I have some thoughts and ideas on **solving the problems on multiple package managers in a principled way**. I shared some early observations in recent NJPLS’25 (my slide). While that talk is on a structural perspective, I’ve since refined a more behavior-oriented understanding, largely inspired by this Z3 experience. Package managers appear to be a system problem, dealing with artifacts e.g. packages, file systems, native binaries, linkers and loaders, however, from the PL person’s perspective, they are merely disguised records with rules of binding and resolving. The problems and solutions can be clearly explained. The future checks, say how to ensure the system-wide z3 is safe, can be done in a principled way. I chatted about ideas with Nikolaj Bjorner and @mgree, and I would also like to share more if anyone is interested, once I finish tidying up the notes and materials.