Skip to content
New issue

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

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

Already on GitHub? # 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.

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

Successfully merging this pull request may close these issues.

3 participants