Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

yasuo-ozu
Copy link

@yasuo-ozu yasuo-ozu commented Sep 11, 2023

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

  • linux-x86_64
  • macOS-x86_64
  • macOS-aarch64 -- no ci test
  • windows-x86_64-msvc
  • windows-x86-msvc -- no ci test

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
Copy link
Contributor

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

@wtdcode
Copy link

wtdcode commented Sep 11, 2023

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

@yasuo-ozu
Copy link
Author

@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
Copy link
Author

@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.

@wtdcode
Copy link

wtdcode commented Sep 11, 2023

@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
Copy link
Author

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
Copy link
Author

@waywardmonkeys any updates?

@waywardmonkeys
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants