Use precompiled z3 libs by default

[Trolldemorted]

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 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 behind a feature gate

CI changes

• Add Windows builds
• Run tests on default, dynamic and static builds for all platforms
• 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) 🎉
• 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]

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

[waywardmonkeys]

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]

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]

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]

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]

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]

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

[Trolldemorted]

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]

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

[connorskees]

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]

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]

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]

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