z3.rs
z3.rs copied to clipboard
prove-rs
`NotExist("/opt/homebrew/Cellar/z3/4.13.0/include/z3.h")` error on macos
Apologies if I've missed an easy solution. On MacOS (15.3.2 Sequoia on M3) I get the following error when adding this to a Rust project:
$ cargo build
Blocking waiting for file lock on build directory
Compiling z3-sys v0.8.1
error: failed to run custom build command for `z3-sys v0.8.1`
Caused by:
process didn't exit successfully: `/Users/caleb/<my_project>/target/debug/build/z3-sys-2589da465cd26a1c/build-script-build` (exit status: 101)
--- stdout
cargo:rerun-if-changed=build.rs
cargo:rerun-if-env-changed=Z3_SYS_Z3_HEADER
cargo:rerun-if-changed=/opt/homebrew/Cellar/z3/4.13.0/include/z3.h
cargo:rerun-if-env-changed=TARGET
cargo:rerun-if-env-changed=BINDGEN_EXTRA_CLANG_ARGS_aarch64-apple-darwin
cargo:rerun-if-env-changed=BINDGEN_EXTRA_CLANG_ARGS_aarch64_apple_darwin
cargo:rerun-if-env-changed=BINDGEN_EXTRA_CLANG_ARGS
--- stderr
thread 'main' panicked at /Users/caleb/.cargo/registry/src/index.crates.io-6f17d22bba15001f/z3-sys-0.8.1/build.rs:47:14:
Unable to generate bindings: NotExist("/opt/homebrew/Cellar/z3/4.13.0/include/z3.h")
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
This suggests that the build file cannot find my Z3 installation, but the options here didn't seem to work for me. I have done brew install z3 and the installation suggests adding the bundled or vcpkg features, but when I do this I get:
the package <name> depends on `z3`, with features: `bundled` but `z3` does not have these features.
failed to select a version for `z3` which could resolve this conflict
Any idea what might be causing this error?
Thanks! Caleb
I think I just need to point it to the latest z3?
ls /opt/homebrew/Cellar/z3/
4.14.1
Update: I was able to fix this for my setup as follows:
- view the version of Z3 that z3-rs is expecting:
$ echo $Z3_SYS_Z3_HEADER
/opt/homebrew/Cellar/z3/4.13.0/include/z3.h
- view the version of Z3 on my system:
$ ls /opt/homebrew/Cellar/z3
4.14.1
- update the value to the version on my system:
$ Z3_SYS_Z3_HEADER=/opt/homebrew/Cellar/z3/4.14.1/include/z3.h
- with the environment variable updated, rerun cargo build:
cargo build
I would be happy to try to help update some of the instructions surrounding this
- would it be helpful to put in a pull request to update the README file here?
Thanks!
Hmm guess I have not fully figured this out yet... 😬
error: linking with `cc` failed: exit status: 1
|
= note: env -u IPHONEOS_DEPLOYMENT_TARGET -u TVOS_DEPLOYMENT_TARGET -u XROS_DEPLOYMENT_TARGET LC_ALL="C" PATH="/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/bin:/opt/anaconda3/bin:/opt/anaconda3/condabin:/usr/local/Cellar/ruby/2.4.1_1/bin:/opt/homebrew/bin:/opt/homebrew/sbin:/usr/local/bin:/System/Cryptexes/App/usr/bin:/usr/bin:/bin:/usr/sbin:/sbin:/var/run/com.apple.security.cryptexd/codex.system/bootstrap/usr/local/bin:/var/run/com.apple.security.cryptexd/codex.system/bootstrap/usr/bin:/var/run/com.apple.security.cryptexd/codex.system/bootstrap/usr/appleinternal/bin:/Users/caleb/.cargo/bin:/Users/caleb/.rvm/bin" VSLANG="1033" ZERO_AR_DATE="1" "cc" "/var/folders/7t/zx2kyf4j7v7223m8cc433g4w0000gn/T/rustcXu0z7N/symbols.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.08k80q6iexl9qamzda5rz4k81.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.0l2keawj9yd5q21ve35c2lutd.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.1c57cwsnp4qplnl0fk4tnebi1.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.1d09pxknd7nn9ch6wb5qx5ndu.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.1of8ubza3m875inrdkyhlqmds.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.2amkaknyzbt56sm59isbgvzbm.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.2nxwx20o10zu6fuclhfz3f21d.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.3aoyw5qk274vox26xytbhg3d9.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.3ltt9riep589hhx7rg8vn2u5t.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.4lf37aytr5va5ejlhe2snej36.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.556t83rvek1wxm14m0tnnxqtq.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.56se70szb0djar8y8ty7xi6cm.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.592esfc2o6i4pzxtpggewdtwl.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.5kut8x4bbq6vb7dxmapvbj85i.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.5rc2lgaqj3tvrqlhf2iles316.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.5watjx8kkt6n0vl9dfx8byxon.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.6hb6fggojqvxmtn8yxngixih7.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.6s591wfb3hqb9ninmiktivh9p.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.715y00ilvhzru33b8ejrrq75s.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.7gudzs4r5rif2hrmd0i82eief.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.7ikhlpgi1w5thj841f2xb8eu5.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.7s14xgwycveew1dhv5j0zcnhb.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.80d1l0x84c6o9m9xc8qzpj27s.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.8bf5gm0sxjv5w9kg1mzmjh1jo.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.8nj7pl4luaq2cgqtq2nqgu52y.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.8p0ybbyrylyxzraprryohka65.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.8v36u41xc8cr1v27mftm48ij4.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.92qvlj5xfxgdfg0h7t1y43co5.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.9l1ul7zz1xfh9sjb7cv2kd2kr.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.9mjmkaagowrcalhd7ey4fy97a.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.a6qjbdlx88xcak3c5ywuidnpl.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.a9krohuws4dfecnnnt19vf2hk.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.amctiec8upkzg52p1gcv6igzf.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.d5pmt0bgcfd2bx90bp75mqq6c.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.eo2s6holo20ddzv5k9e9sn696.rcgu.o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c.0hcke9w4dtf6vilwo3r8at72s.rcgu.o" "/Users/caleb/git/project/target/debug/deps/libstructopt-c98e329dc559375a.rlib" "/Users/caleb/git/project/target/debug/deps/liblazy_static-4b0dd91e51bc9b12.rlib" "/Users/caleb/git/project/target/debug/deps/libclap-57dd631440301825.rlib" "/Users/caleb/git/project/target/debug/deps/libvec_map-57bf1a9e55a64b0b.rlib" "/Users/caleb/git/project/target/debug/deps/libtextwrap-ad983b3d914d628e.rlib" "/Users/caleb/git/project/target/debug/deps/libunicode_width-2ffdc61ba0d8fe17.rlib" "/Users/caleb/git/project/target/debug/deps/libstrsim-cd460e502608f23d.rlib" "/Users/caleb/git/project/target/debug/deps/libbitflags-ffac5189631c5c4e.rlib" "/Users/caleb/git/project/target/debug/deps/libatty-069c12a4063bb144.rlib" "/Users/caleb/git/project/target/debug/deps/liblibc-520847c14b193997.rlib" "/Users/caleb/git/project/target/debug/deps/libansi_term-04e635d149bbf30f.rlib" "/Users/caleb/git/project/target/debug/deps/libproject-6b88a5565e420d11.rlib" "/Users/caleb/git/project/target/debug/deps/libz3-acb0197cb5b909c5.rlib" "/Users/caleb/git/project/target/debug/deps/libz3_sys-a1da6e9cd95f6b48.rlib" "/Users/caleb/git/project/target/debug/deps/liblog-02f6195e154e37e2.rlib" "/Users/caleb/git/project/target/debug/deps/libnum_bigint-3b7accf606e6fd90.rlib" "/Users/caleb/git/project/target/debug/deps/libnum_integer-1cb330cc3208d9c8.rlib" "/Users/caleb/git/project/target/debug/deps/libnum_traits-c608e80f7fc11135.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libstd-83616591c03b4bdb.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libpanic_unwind-ebf901b6d23bf634.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libobject-7710b4452bd82af9.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libmemchr-f98cf7c088667f19.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libaddr2line-6392ea87905caffc.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libgimli-25a08af37ed77b0e.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/librustc_demangle-284c364e42397f3c.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libstd_detect-0ca552d44faec676.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libhashbrown-3d585033511079b9.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/librustc_std_workspace_alloc-6619a2e13d28fdc8.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libminiz_oxide-6ed5108eff20a13b.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libadler-4dc30e5b1322c3d7.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libunwind-1abf6f4ec08a1e84.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libcfg_if-189cd29769b1eb60.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/liblibc-b73012c1f7d960db.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/liballoc-60825299673ba243.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/librustc_std_workspace_core-0ffffa7eb0407c16.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libcore-ec2fdc463bb543f6.rlib" "/Users/caleb/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/aarch64-apple-darwin/lib/libcompiler_builtins-d6d5c321a716d6df.rlib" "-lc" "-lm" "-liconv" "-lz3" "-lSystem" "-lc" "-lm" "-arch" "arm64" "-mmacosx-version-min=11.0.0" "-o" "/Users/caleb/git/project/target/debug/deps/project-1a2b6992dfdf811c" "-Wl,-dead_strip" "-nodefaultlibs"
= note: ld: warning: ignoring duplicate libraries: '-lc', '-lm'
ld: warning: search path '/opt/homebrew/Cellar/z3/4.13.0/lib' not found
ld: library 'z3' not found
clang: error: linker command failed with exit code 1 (use -v to see invocation)
ok I just cloned my new z3 version to the expected old location... now it works!
cp -r /opt/homebrew/Cellar/z3/4.14.1 /opt/homebrew/Cellar/z3/4.13.0
Hi, I think the improvements to the readme in #364 as well as the new gh-release feature in #352 should address your issues. Let me know!
Nice, thanks for taking a look! I don't have a setup to test at present but next time I am adding z3-rs as a dependency on a fresh machine, I will post an update here if the newREADME installation instructions worked.