Rethink Builds

[toolCHAINZ]

Some recent discussion #498 has made me start thinking again about how this library is built. The current system (http fetch of the z3 ref and subsequent download) works but is brittle and requires lots of extra build dependencies.

I'm thinking we should instead use something like the following setup:

We add an new crate, z3-src (I've already squatted the name, just in case), inspired by openssl-src, which contains the z3 source tree and the logic needed to build it. z3-sys will then hold the low-level bindings and bindgen glue. It will build as it does now, dynamically linking against the system z3, against a github-sourced binary with gh-release, or against the library produced by z3-src through a new vendored feature flag.

This lets us:

• remove the z3 submodule
• remove all "fetch sources from github" logic currently in bundled
• easily allow users to target different z3 versions by targeting different versions of z3-src
• separate the currently-entangled concerns of building z3 (now handled by z3-src), running bindgen, and setting up linker paths.

As a separate discussion, per #498, we may want to track z3 versions more closely; in such a case maybe it make sense to track the current dynamic bindgen stuff in version control? Doing so would remove more annoying build dependencies for users.

Any thoughts @Pat-Lafon @lmondada ?

[Pat-Lafon]

Given something like #498, won't that also alleviate some of these concerns in a different way?

Rust bindings are now in tree so a little less of the submodule issues. Instead of fetching from github, it seems like they just package z3 source https://pypi.org/project/z3-solver/#z3_solver-4.16.0.0.tar.gz alongside the bindings(I assume this means if you want different versions of z3, you can pull in different versions of the python bindings since they are tightly connected). On the other hand, sadly it seems like there is very little to no support for using system z3 or some of the alternative install paths: Z3Prover/z3#491, https://discuss.ocaml.org/t/ask-for-suggestions-for-the-next-z3-package-release/8922/17, Z3Prover/z3#7035.

I have noticed another pattern where you gate different parts of the api behind feature flags like what Inkwell does for llvm. To be clear, this is a lot of work and particularly because LLVM frequently ships breaking changes so I wouldn't recommend that necessarily.

Maybe all is to say, I'm intrigued by the different possible packaging options. I don't have too strong of an opinion. How important is version selection for Z3 versus only supporting latest + whatever your system installer provides?

[toolCHAINZ]

Yeah, going in-tree to z3 would necessitate this type of setup I think. Like the issues you linked indicate, in the case of python, z3 upstream builds wheels for every supported platform with a hard coded z3 shared object and load library path, making retargeting another version impossible without finding/building a wheel.

Yeah, I did the flag thing as a stop gap until Ubuntu bumps its z3 version this April. Then I think we can remove all those (and I as well would rather not add more).

I personally don't care too much about being able to link against specific old versions, I'm just mentioning it as something we should support because the last downstream project I interacted with did specifically want to link against 4.15.3.

If we get to a high level of API coverage and sync version numbers, and the bindings "stabilize" then I think maybe this concern won't matter as much. Then users could just specify exactly the z3 version they want to work with and use vendored. (This is looking forward to some point in the future where people aren't trying to target anything older than 4.16.0)

[Pat-Lafon]

Yeah, sounds fair. I have heard of people targeting older Z3 versions because sometimes there are small changes that drastically affect query solve times(I think for dafny at one point they pinned to a specific older version of Z3). In contrast, I would hope that most people can just use the latest since the Z3 c api doesn't change all that much in terms of breaking changes.

Moving towards something that can be in-tree would be super cool. Maybe that would make development/fixes a little harder but it would be a nice show of first-class support.

[toolCHAINZ]

$ cargo package --allow-dirty
   Packaging z3-src v0.1.0 (/Users/user/RustroverProjects/z3.rs/z3-src)
    Updating crates.io index
    Packaged 2649 files, 28.3MiB (5.8MiB compressed)

It's big, but the compressed file-size limit is 10 megs, so I think this strategy would actually work. I had claude to a quick translation of the z3-sys build.rs logic into z3-src, which is now invoked by the z3-sys/bundled feature instead of manually running cmake.

[toolCHAINZ]

Some WIP code in #510.
Also experimenting with checking in the generated headers to avoid the bindgen dep