prove-rs / z3.rs

Rust bindings for the Z3 solver.
347 stars 110 forks source link

Use downloaded Z3 binary by default when `static-link-z3` flag is active #249

Open yasuo-ozu opened 1 year ago

yasuo-ozu commented 1 year ago

Replace #193 Includes #207

This PR adds feature flag static-link-z3 and force-build-z3 to change building behavior of z3-sys.

static-link-z3 force-build-z3 behavior
off off Use system binary (dynamic link)
on off If supported, static link with precompiled binary. Otherwise, same as force-build-z3
on on Compile z3 using bundled z3 source tree and link statically

Precompiled binary support

For environments with no precompiled binary support, automatically fallback to force-build-z3

Build time

environment system precompoled build
linux-x86_64 43s 1m45 16m1
windows-x86_64-msvc 1m36 3m20 27m16
macos-x86_64 1m25 2m36 17m6
waywardmonkeys commented 1 year ago

Not sure if this would be interesting to you or not, but have you considered also supporting vcpkg (especially for Windows)?

wtdcode commented 1 year ago

Most Linux distributions and macOS homebrew offer precompiled z3 libraries so there is no need to fallback to building manually.

yasuo-ozu commented 1 year ago

@waywardmonkeys I'm sorry that I don't know about vcpkg. What do you mean by "supporting vcpkg"?

In my understanding, the precompiled z3 requires msvc's C++ runtime such as msvcp140.dll, msvcp140_1.dll, msvcp140_2.dll, ... This PR assumes the precondition that C++ runtime is already installed on the Windows system. I think the following lines in .github/workflows/rust.yml is enough for now.

        choco install vcredist2017
        echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV
yasuo-ozu commented 1 year ago

@wtdcode

no need to fallback to building manually

I don't think so. Considering Rust projects which depends on z3-sys with static-link-z3 flag, users who we cannot offer precompiled binary for, should have to do followings:

https://doc.rust-lang.org/cargo/reference/overriding-dependencies.html

This is not smart way, so I think the fallback is better.

wtdcode commented 1 year ago

@wtdcode

no need to fallback to building manually

I don't think so. Considering Rust projects which depends on z3-sys with static-link-z3 flag, users who we cannot offer precompiled binary for, should have to do followings:

  • Install z3 package with their package manager (sometimes difficult as if they are not super user)
  • Disable static-link-z3 flag manually with overriding z3-sys dependenciy in Cargo.toml

https://doc.rust-lang.org/cargo/reference/overriding-dependencies.html

This is not smart way, so I think the fallback is better.

Oh I misunderstood your statements and didn’t check the code. You are correct on this.

But further I suggest using pkg-config like my PR to avoid so many hardcoded paths.

yasuo-ozu commented 1 year ago

I suggest using pkg-config like my PR to avoid so many hardcoded paths

I agree. (It can be implemented with new PR.)

yasuo-ozu commented 1 year ago

@waywardmonkeys any updates?

waywardmonkeys commented 1 year ago

I am hoping to get back to this this week. Support for vcpkg has landed which helps on Windows. I would like to do some other cleanups to the build and then look at this.