Use precompiled z3 libs by default

Trolldemorted commented 2 years ago

Fixes https://github.com/prove-rs/z3.rs/issues/192 https://github.com/prove-rs/z3.rs/issues/183 https://github.com/prove-rs/z3.rs/issues/87 https://github.com/prove-rs/z3.rs/issues/224 https://github.com/prove-rs/z3.rs/issues/212 and most likely https://github.com/prove-rs/z3.rs/issues/172

This PR tries to solve a number of rough edges of z3-sys mentioned in https://github.com/prove-rs/z3.rs/issues/192:

Structural changes

Changes the default build to link against libraries downloaded from https://github.com/Z3Prover/z3/releases.
Move bindgen out of z3-sys

CI changes

Add Windows builds
Run tests on default, dynamic and static builds for all platforms where it works
Stop ignoring errors in CI

QOL changes

Default installation needs no manual steps and yet does not rebuild z3
z3-sys with the default features is now completely dependency free (except for z3 itself, ureq and zip) 🎉
Switching to more coarse conditional compilation in build.rs to increased the readability in my opinion

Negative aspects

So far I threw x86 out. Do you know whether anyone is still using it?
~cargo test does not execute doc examples because they fail due to a cargo bug: https://github.com/rust-lang/cargo/issues/8531~
Version bumps of z3 must be done in multiple files, and the bindgen output must match the version

What do you think? I didn't touch the documentation yet, because I wanted to hear your opinion on the technical side of things first.

Bickio commented 2 years ago

I was unable to build using latest master and the commit in this PR solved my issue. +1 for merging this change

waywardmonkeys commented 2 years ago

The issues with compile times and version fragility have been bothering me a lot as well. I started to wonder "Can we fix the compile time of Z3 itself?" and took a look, but it ends up that that is hard to fix as well.

I think we'll have to sort out a way to have the doc tests run. I've been hoping to add more of those and get rid of some of the standalone tests, so that the docs are more useful.

This PR is using bindgen 0.59, but should move to 0.60, to use the current version (and match what is on the head branch of z3-sys).

Using system-provided Z3 is still problematic in the near future as that is 4.8.x and we'll be wanting to move the bindings forward to using more recent versions of Z3 and supporting the newer APIs that have been added. But that's separate from this, except that having this use the pre-compiled binaries makes the compilation times acceptable.

I'd like to see this move forward for sure.

What're the next steps and is there anything I can do to help?

waywardmonkeys commented 2 years ago

It might be worth cherry-picking the parts to use pre-compiled libs before making changes to the bindgen stuff or at least separately from it?

Or if they're too inter-related and both are needed at once, then we just leave this as it is.

waywardmonkeys commented 2 years ago

I was unable to build using latest master and the commit in this PR solved my issue. +1 for merging this change

What build error are you seeing with the latest master?

Bickio commented 2 years ago

What build error are you seeing with the latest master?

Linux Mint 20.2

  wrapper.h:1:10: fatal error: 'z3.h' file not found
  wrapper.h:1:10: fatal error: 'z3.h' file not found, err: true
  thread 'main' panicked at 'Unable to generate bindings: ()', /home/bickio/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/build.rs:33:14

Can provide the full backtrace if required

Edit: with static-link-z3 I get this:

CMake Warning at CMakeLists.txt:51 (message):
    Disabling Z3_INCLUDE_GIT_DESCRIBE
  Call Stack (most recent call first):
    CMakeLists.txt:100 (disable_git_describe)

  CMake Warning at CMakeLists.txt:55 (message):
    Disabling Z3_INCLUDE_GIT_HASH
  Call Stack (most recent call first):
    CMakeLists.txt:101 (disable_git_hash)

  make: warning: -j12 forced in submake: resetting jobserver mode.
  INFO:root:Generated "/<project folder>/target/debug/build/z3-sys-d51a165876161722/out/build/src/api/dll/install_tactic.cpp"
  /usr/include/stdio.h:33:10: fatal error: 'stddef.h' file not found
  /usr/include/stdio.h:33:10: fatal error: 'stddef.h' file not found, err: true
  thread 'main' panicked at 'Unable to generate bindings: ()', /home/bickio/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/build.rs:33:14

waywardmonkeys commented 2 years ago

Thanks, @Bickio

I'm looking at the original changes in this PR and have found a few issues ... I'll try and land something by Monday or Tuesday that addresses all of this, with these changes as a starting point.

waywardmonkeys commented 2 years ago

@Bickio I haven't forgotten. Something else came up this week and I'm a bit behind.

Trolldemorted commented 2 years ago

It might be worth cherry-picking the parts to use pre-compiled libs before making changes to the bindgen stuff or at least separately from it?

I guess it depends on how early you want to ship the next release, for my personal stuff I can continue with my fork until something like this lands upstream, so I don't have overly urgent time pressure.

Trolldemorted commented 1 year ago

Any chance we can get this (or a similar implementation) upstream at some point? 😇

connorskees commented 1 year ago

My use case is running this library on a somewhat under-powered server, where when trying to build z3 LLVM runs for several minutes until it fails due to OOM. Using this branch lets my project build successfully.

Trolldemorted commented 1 year ago

Done some changes:

rebased onto master
added CI for static and default macos builds
moved bindgen out of z3-sys to reduce z3 rebuilds
moved the bindgen output to target-specific folders, since the bindgen output on different targets is not equal
replaced curl, unzip and tar with the ureq and zip crates
halved CI runtime by no longer building z3 twice
"fix" doctests by working around https://github.com/rust-lang/cargo/issues/8531

I have no idea how builds and CI tests for native z3 installations on macos would look like, because master does not have them either. Since you had to disable tests for native z3 installations for ubuntu on master, I sincerely recommend scrapping that feature completely. We will never get it safe, and at some point it is going to hurt someone.

@waywardmonkeys PTAL, the current state of master is disadvantageous :)

Trolldemorted commented 1 year ago

I am sorry for the late response, but I won't have sufficient free time to complete this pull request in the near future.

You are of cause very welcome to pick any contribution here, and integrate it into the current master.

In the long run you might want to find out whether you are allowed to redistribute z3 binaries (then you could drop the download and extraction), and decide and announce whether you want to keep the non-optional dependency on bindgen, which prevents users from building z3.rs on systems without a clang installation.

I will keep my branch in the current state, so those affected by the mentioned issues have a workaround for the time being.

stefnotch commented 1 year ago

@waywardmonkeys I would hate to see this PR go to waste. Is there a reasonable way forward for this?

prove-rs / z3.rs