Skip to content

Rename static-link-z3 to bundled. #260

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

Merged
merged 2 commits into from
Oct 27, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions .github/workflows/rust.yml
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ jobs:
# XXX: Ubuntu's Z3 package seems to be missing some symbols, like
# `Z3_mk_pbeq`, leading to linker errors. Just ignore this, I guess, until
# we figure out how to work around it. At least we have the
# statically-linked Z3 tests below...
# build using a bundled Z3 below...
if: ${{ success() || failure() }}

build_on_wasm:
Expand All @@ -57,12 +57,12 @@ jobs:
source ./emsdk_env.sh
- name: Install wasm32-unknown-emscripten target
run: rustup target add wasm32-unknown-emscripten
- name: Build z3-sys and z3 with statically linked Z3
- name: Build z3-sys and z3 with bundled Z3
run: |
source ~/emsdk/emsdk_env.sh
cargo build --target=wasm32-unknown-emscripten --features static-link-z3
cargo build --target=wasm32-unknown-emscripten --features bundled

build_z3_statically:
build_with_bundled_z3:
strategy:
matrix:
build: [linux, macos, windows]
Expand All @@ -87,8 +87,8 @@ jobs:
- name: Set LIBCLANG_PATH
run: echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV
if: matrix.os == 'windows-latest'
- name: Test `z3-sys` and `z3` with statically linked Z3
run: cargo test --workspace --features static-link-z3
- name: Test `z3-sys` and `z3` with bundled linked Z3
run: cargo test --workspace --features bundled

build_with_vcpkg_installed_z3:
strategy:
Expand Down
10 changes: 6 additions & 4 deletions z3-sys/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,9 @@ cmake = { version = "0.1.49", optional = true }
vcpkg = { version = "0.2.15", optional = true }

[features]
# Enable this feature to statically link our own build of Z3, rather than
# dynamically linking to the system's `libz3.so`.
static-link-z3 = ["cmake"]
vcpkg = ["dep:vcpkg"]
bundled = ["dep:cmake"] # Build Z3 via our bundled submodule.
vcpkg = ["dep:vcpkg"] # Build Z3 via vcpkg.

# Legacy feature for short term compatibility
static-link-z3 = ["bundled", "deprecated-static-link-z3"]
deprecated-static-link-z3 = []
32 changes: 23 additions & 9 deletions z3-sys/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,18 +24,32 @@ Add it to your `Cargo.toml` like so:
z3-sys = "0.8"
```

**Note:** This crate requires a `z3.h` during build time.
### Finding Z3 Libraries

* By default, the crate will look for a `z3.h` in standard/system include paths.
* If the feature `static-link-z3` is enabled, the `z3.h` of the built Z3 will be used.
* Alternatively, the path to the desired `z3.h` can be specified via the environment variable
`Z3_SYS_Z3_HEADER`. I.e., running:
**Note:** This library has a dependency on Z3.

```console
$ Z3_SYS_Z3_HEADER="/path/to/my/z3.h" cargo build
```
There are 3 ways for this crate to currently find Z3:

* By default, it will look for a system-installed copy of Z3.
On Linux, this would be via the package manager. On macOS, this
might be via Homebrew (`brew install z3`).
* Enabling the `bundled` feature will use `cmake` to build a
locally bundled copy of Z3. This copy is provided via a git
submodule within the repository.
* Enabling the `vcpkg` feature will use `vcpkg` to build and
install a copy of Z3 which is then used.

**Note:** This crate requires a `z3.h` during build time.

in your project will use `/path/to/my/z3.h` instead.
* By default, the crate will look for a `z3.h` in standard/system
include paths. The `Z3_SYS_Z3_HEADER` environment variable can
also be used to customize this.
* Enabling the`bundled` feature will cause the bundled copy of `z3.h`
to be used. The `Z3_SYS_Z3_HEADER` environment variable can also
be used to customize this.
* Enabling the `vcpkg` feature will cause the copy of `z3.h` provided
by that version to be used. In this case, there is no override
via the environment variable.

## Support and Maintenance

Expand Down
14 changes: 7 additions & 7 deletions z3-sys/build.rs
Original file line number Diff line number Diff line change
@@ -1,16 +1,17 @@
use std::env;

fn main() {
// Feature `vcpkg` is prior to `static-link-z3` as vcpkg-installed z3 is also statically linked.

#[cfg(not(feature = "vcpkg"))]
#[cfg(feature = "static-link-z3")]
#[cfg(feature = "bundled")]
build_bundled_z3();

#[cfg(feature = "deprecated-static-link-z3")]
println!("cargo:warning=The 'static-link-z3' feature is deprecated. Please use the 'bundled' feature.");

println!("cargo:rerun-if-changed=build.rs");

#[cfg(not(feature = "vcpkg"))]
let header = find_header_by_env();

#[cfg(feature = "vcpkg")]
let header = find_library_header_by_vcpkg();

Expand Down Expand Up @@ -69,7 +70,7 @@ fn find_library_header_by_vcpkg() -> String {
#[cfg(not(feature = "vcpkg"))]
fn find_header_by_env() -> String {
const Z3_HEADER_VAR: &str = "Z3_SYS_Z3_HEADER";
let header = if cfg!(feature = "static-link-z3") {
let header = if cfg!(feature = "bundled") {
"z3/src/api/z3.h".to_string()
} else if let Ok(header_path) = env::var(Z3_HEADER_VAR) {
header_path
Expand Down Expand Up @@ -116,8 +117,7 @@ fn generate_binding(header: &str) {
}

/// Build z3 with bundled source codes.
#[cfg(not(feature = "vcpkg"))]
#[cfg(feature = "static-link-z3")]
#[cfg(feature = "bundled")]
fn build_bundled_z3() {
let mut cfg = cmake::Config::new("z3");
cfg
Expand Down
9 changes: 4 additions & 5 deletions z3/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,12 @@ edition = "2018"

[features]
default = []

# Enable this feature to statically link our own build of Z3, rather than
# dynamically linking to the system's `libz3.so`.
static-link-z3 = ["z3-sys/static-link-z3"]

bundled = ["z3-sys/bundled"]
vcpkg = ["z3-sys/vcpkg"]

# This is a legacy feature here for short term compatibility.
static-link-z3 = ["z3-sys/bundled", "z3-sys/deprecated-static-link-z3"]

[dependencies]
log = "0.4"

Expand Down
28 changes: 24 additions & 4 deletions z3/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,33 @@ Add it to your `Cargo.toml` like so:
z3 = "0.12"
```

**Note:** This library has a dependency on Z3. You will either need to
have the Z3 dependency already installed, or you can statically link
to our build of Z3 like so:
### Finding Z3 Libraries

**Note:** This library has a dependency on Z3.

There are 3 ways for this crate to currently find Z3:

* By default, it will look for a system-installed copy of Z3.
On Linux, this would be via the package manager. On macOS, this
might be via Homebrew (`brew install z3`).
* Enabling the `bundled` feature will use `cmake` to build a
locally bundled copy of Z3. This copy is provided via a git
submodule within the repository.
* Enabling the `vcpkg` feature will use `vcpkg` to build and
install a copy of Z3 which is then used.

This might look like:

```toml
[dependencies]
z3 = {version="0.12", features = ["bundled"]}
```

or:

```toml
[dependencies]
z3 = {version="0.12", features = ["static-link-z3"]}
z3 = {version="0.12", features = ["vcpkg"]}
```

## Support and Maintenance
Expand Down