diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index c4c35472..387a48f9 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -94,6 +94,55 @@ jobs: run: cargo test -vv --features static-link-z3 - name: Test `z3` with statically linked Z3 and `arbitrary-size-numeral` enabled run: cargo test --manifest-path z3/Cargo.toml -vv --features 'static-link-z3 arbitrary-size-numeral' + build_with_vcpkg_installed_z3: + strategy: + matrix: + build: [windows] # [linux, macos, windows] + include: + # - build: linux + # os: ubuntu-latest + # vcpkg_triplet: x64-linux + # - build: macos + # os: macos-latest + # vcpkg_triplet: x64-osx + - build: windows + os: windows-latest + vcpkg_triplet: x64-windows-static-md + runs-on: ${{ matrix.os }} + env: + VCPKG_ROOT: ${{ github.workspace }}/vcpkg + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + - name: Install LLVM and Clang # required for bindgen to work, see https://github.com/rust-lang/rust-bindgen/issues/1797 + uses: KyleMayes/install-llvm-action@v1 + if: matrix.os == 'windows-latest' + with: + version: "11.0" + directory: ${{ runner.temp }}/llvm + - name: Set LIBCLANG_PATH + run: echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV + if: matrix.os == 'windows-latest' + - run: echo Instaling z3:${{ matrix.vcpkg_triplet }} on ${{ matrix.os }}. + - name: vcpkg build z3 + uses: johnwason/vcpkg-action@v5 + id: vcpkg + with: + pkgs: z3 + triplet: ${{ matrix.vcpkg_triplet }} + cache-key: ${{ matrix.os }} + revision: master + token: ${{ github.token }} + extra-args: --clean-buildtrees-after-build + - name: Show default toolchain of rust. + run: rustup default + - name: Build `z3-sys` and `z3` with vcpkg installed Z3 + run: cargo build -vv --features vcpkg + - name: Test `z3-sys` and `z3` with vcpkg installed Z3 + run: cargo test -vv --features vcpkg + - name: Test `z3` with vcpkg installed Z3 and `arbitrary-size-numeral` enabled + run: cargo test --manifest-path z3/Cargo.toml -vv --features 'vcpkg arbitrary-size-numeral' run_clippy: runs-on: ubuntu-latest diff --git a/z3-sys/Cargo.toml b/z3-sys/Cargo.toml index bb2ec14b..495e0334 100644 --- a/z3-sys/Cargo.toml +++ b/z3-sys/Cargo.toml @@ -18,8 +18,10 @@ repository = "https://github.com/prove-rs/z3.rs.git" [build-dependencies] bindgen = { version = "0.66.0", default-features = false, features = ["runtime"] } 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"] diff --git a/z3-sys/build.rs b/z3-sys/build.rs index 010c1aeb..1614a9bb 100644 --- a/z3-sys/build.rs +++ b/z3-sys/build.rs @@ -1,13 +1,45 @@ use std::env; +#[cfg(not(feature = "vcpkg"))] const Z3_HEADER_VAR: &str = "Z3_SYS_Z3_HEADER"; 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")] - build_z3(); + build_bundled_z3(); 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(); + + generate_binding(&header); +} + +#[cfg(feature = "vcpkg")] +fn find_library_header_by_vcpkg() -> String { + let lib = vcpkg::Config::new() + .emit_includes(true) + .find_package("z3") + .unwrap(); + for include in lib.include_paths.iter() { + let mut include = include.clone(); + include.push("z3.h"); + if include.exists() { + let header = include.to_str().unwrap().to_owned(); + println!("cargo:rerun-if-changed={}", header); + return header; + } + } + panic!("z3.h is not found in include path of installed z3."); +} + +#[cfg(not(feature = "vcpkg"))] +fn find_header_by_env() -> String { let header = if cfg!(feature = "static-link-z3") { "z3/src/api/z3.h".to_string() } else if let Ok(header_path) = std::env::var(Z3_HEADER_VAR) { @@ -17,6 +49,10 @@ fn main() { }; println!("cargo:rerun-if-env-changed={}", Z3_HEADER_VAR); println!("cargo:rerun-if-changed={}", header); + header +} + +fn generate_binding(header: &str) { let out_path = std::path::PathBuf::from(std::env::var("OUT_DIR").unwrap()); for x in &[ @@ -31,7 +67,7 @@ fn main() { "symbol_kind", ] { let mut enum_bindings = bindgen::Builder::default() - .header(&header) + .header(header) .parse_callbacks(Box::new(bindgen::CargoCallbacks)) .generate_comments(false) .rustified_enum(format!("Z3_{}", x)) @@ -50,8 +86,10 @@ fn main() { } } +/// Build z3 with bundled source codes. +#[cfg(not(feature = "vcpkg"))] #[cfg(feature = "static-link-z3")] -fn build_z3() { +fn build_bundled_z3() { let mut cfg = cmake::Config::new("z3"); cfg // Don't build `libz3.so`, build `libz3.a` instead. diff --git a/z3/Cargo.toml b/z3/Cargo.toml index 483ed66f..11c3c7a3 100644 --- a/z3/Cargo.toml +++ b/z3/Cargo.toml @@ -21,6 +21,8 @@ arbitrary-size-numeral = ["num"] # dynamically linking to the system's `libz3.so`. static-link-z3 = ["z3-sys/static-link-z3"] +vcpkg = ["z3-sys/vcpkg"] + [dependencies] log = "0.4"