search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
351 stars 113 forks source link

Build failures on fedora when building and statically linking our own Z3 #98

Closed fitzgen closed 4 years ago

fitzgen commented 4 years ago

@julian-seward1 could you provide the output of running cargo build -vv --features static-link-z3 from within the z3-sys directory here? Thanks!

julian-seward1 commented 4 years ago

It fails thusly:

     Running `/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-768ceade83050802/build-script-build`
[z3-sys 0.6.2] running: "cmake" "/home/sewardj/MOZ/WT/RMME/z3.rs/z3-sys/z3" "-DZ3_BUILD_LIBZ3_SHARED=false" "-DZ3_BUILD_EXECUTABLE=false" "-DZ3_BUILD_TEST_EXECUTABLES=false" "-DCMAKE_INSTALL_PREFIX=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out" "-DCMAKE_C_FLAGS= -ffunction-sections -fdata-sections -fPIC -m64" "-DCMAKE_C_COMPILER=/usr/lib64/ccache/cc" "-DCMAKE_CXX_FLAGS= -ffunction-sections -fdata-sections -fPIC -m64" "-DCMAKE_CXX_COMPILER=/usr/lib64/ccache/c++" "-DCMAKE_ASM_FLAGS= -ffunction-sections -fdata-sections -fPIC -m64" "-DCMAKE_ASM_COMPILER=/usr/lib64/ccache/cc" "-DCMAKE_BUILD_TYPE=Debug"
[z3-sys 0.6.2] CMake Error: The source directory "/home/sewardj/MOZ/WT/RMME/z3.rs/z3-sys/z3" does not appear to contain CMakeLists.txt.
[z3-sys 0.6.2] Specify --help for usage, or press the help button on the CMake GUI.
[z3-sys 0.6.2] thread 'main' panicked at '
[z3-sys 0.6.2] command did not execute successfully, got: exit code: 1
[z3-sys 0.6.2] 
[z3-sys 0.6.2] build script failed, must exit now', /home/sewardj/.cargo/registry/src/github.com-1ecc6299db9ec823/cmake-0.1.44/src/lib.rs:885:5
[z3-sys 0.6.2] note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: failed to run custom build command for `z3-sys v0.6.2 (/home/sewardj/MOZ/WT/RMME/z3.rs/z3-sys)`

Caused by:
  process didn't exit successfully: `/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-768ceade83050802/build-script-build` (exit code: 101)
  --- stdout
  running: "cmake" "/home/sewardj/MOZ/WT/RMME/z3.rs/z3-sys/z3" "-DZ3_BUILD_LIBZ3_SHARED=false" "-DZ3_BUILD_EXECUTABLE=false" "-DZ3_BUILD_TEST_EXECUTABLES=false" "-DCMAKE_INSTALL_PREFIX=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out" "-DCMAKE_C_FLAGS= -ffunction-sections -fdata-sections -fPIC -m64" "-DCMAKE_C_COMPILER=/usr/lib64/ccache/cc" "-DCMAKE_CXX_FLAGS= -ffunction-sections -fdata-sections -fPIC -m64" "-DCMAKE_CXX_COMPILER=/usr/lib64/ccache/c++" "-DCMAKE_ASM_FLAGS= -ffunction-sections -fdata-sections -fPIC -m64" "-DCMAKE_ASM_COMPILER=/usr/lib64/ccache/cc" "-DCMAKE_BUILD_TYPE=Debug"

  --- stderr
  CMake Error: The source directory "/home/sewardj/MOZ/WT/RMME/z3.rs/z3-sys/z3" does not appear to contain CMakeLists.txt.
  Specify --help for usage, or press the help button on the CMake GUI.
  thread 'main' panicked at '
  command did not execute successfully, got: exit code: 1

  build script failed, must exit now', /home/sewardj/.cargo/registry/src/github.com-1ecc6299db9ec823/cmake-0.1.44/src/lib.rs:885:5
  note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
julian-seward1 commented 4 years ago

This is with cmake version 3.17.4.

fitzgen commented 4 years ago

Ah sorry, can you run

git submodule update --init

and then re-run cargo build -vv --features static-link-z3?

julian-seward1 commented 4 years ago

Ok, that does reproduce the link error I saw. Results are as follows.

[z3-sys 0.6.2] [100%] Built target libz3
[z3-sys 0.6.2] Install the project...
[z3-sys 0.6.2] -- Install configuration: "Debug"
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib64/cmake/z3/Z3Targets.cmake
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib64/cmake/z3/Z3Targets-debug.cmake
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib64/cmake/z3/Z3Config.cmake
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib64/cmake/z3/Z3ConfigVersion.cmake
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib64/libz3.a
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_algebraic.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_api.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_ast_containers.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_fixedpoint.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_fpa.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3++.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_macros.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_optimization.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_polynomial.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_rcf.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_v1.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_spacer.h
[z3-sys 0.6.2] -- Installing: /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/include/z3_version.h
[z3-sys 0.6.2] cargo:root=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out
[z3-sys 0.6.2] cargo:rustc-link-lib=stdc++
[z3-sys 0.6.2] cargo:rustc-link-search=native=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib
[z3-sys 0.6.2] cargo:rustc-link-lib=static=z3
     Running `CARGO=/home/sewardj/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/bin/cargo CARGO_CRATE_NAME=z3_sys CARGO_MANIFEST_DIR=/home/sewardj/MOZ/WT/RMME/z3.rs/z3-sys CARGO_PKG_AUTHORS='Graydon Hoare <graydon@pobox.com>:Bruce Mitchener <bruce.mitchener@gmail.com>:Nick Fitzgerald <fitzgen@gmail.com>' CARGO_PKG_DESCRIPTION='Low-level bindings for the Z3 SMT solver from Microsoft Research' CARGO_PKG_HOMEPAGE='https://github.com/prove-rs/z3.rs' CARGO_PKG_LICENSE=MIT CARGO_PKG_LICENSE_FILE='' CARGO_PKG_NAME=z3-sys CARGO_PKG_REPOSITORY='https://github.com/prove-rs/z3.rs.git' CARGO_PKG_VERSION=0.6.2 CARGO_PKG_VERSION_MAJOR=0 CARGO_PKG_VERSION_MINOR=6 CARGO_PKG_VERSION_PATCH=2 CARGO_PKG_VERSION_PRE='' LD_LIBRARY_PATH='/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/deps:/home/sewardj/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib:/home/sewardj/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib:' OUT_DIR=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out rustc --crate-name z3_sys z3-sys/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="cmake"' --cfg 'feature="static-link-z3"' -C metadata=f163e8c31ff48957 -C extra-filename=-f163e8c31ff48957 --out-dir /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/deps -C incremental=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/incremental -L dependency=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/deps -L native=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib -l stdc++ -l static=z3`
error: could not find native static library `z3`, perhaps an -L flag is missing?

error: aborting due to previous error

error: could not compile `z3-sys`.

Caused by:
  process didn't exit successfully: `CARGO=/home/sewardj/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/bin/cargo CARGO_CRATE_NAME=z3_sys CARGO_MANIFEST_DIR=/home/sewardj/MOZ/WT/RMME/z3.rs/z3-sys CARGO_PKG_AUTHORS='Graydon Hoare <graydon@pobox.com>:Bruce Mitchener <bruce.mitchener@gmail.com>:Nick Fitzgerald <fitzgen@gmail.com>' CARGO_PKG_DESCRIPTION='Low-level bindings for the Z3 SMT solver from Microsoft Research' CARGO_PKG_HOMEPAGE='https://github.com/prove-rs/z3.rs' CARGO_PKG_LICENSE=MIT CARGO_PKG_LICENSE_FILE='' CARGO_PKG_NAME=z3-sys CARGO_PKG_REPOSITORY='https://github.com/prove-rs/z3.rs.git' CARGO_PKG_VERSION=0.6.2 CARGO_PKG_VERSION_MAJOR=0 CARGO_PKG_VERSION_MINOR=6 CARGO_PKG_VERSION_PATCH=2 CARGO_PKG_VERSION_PRE='' LD_LIBRARY_PATH='/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/deps:/home/sewardj/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib:/home/sewardj/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib:' OUT_DIR=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out rustc --crate-name z3_sys z3-sys/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="cmake"' --cfg 'feature="static-link-z3"' -C metadata=f163e8c31ff48957 -C extra-filename=-f163e8c31ff48957 --out-dir /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/deps -C incremental=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/incremental -L dependency=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/deps -L native=/home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib -l stdc++ -l static=z3` (exit code: 1)
julian-seward1 commented 4 years ago 
$ ls -l /usr/lib64/*z3*
lrwxrwxrwx. 1 root root       10 May 10 04:48 /usr/lib64/libz3.so -> libz3.so.0*
lrwxrwxrwx. 1 root root       14 May 10 04:48 /usr/lib64/libz3.so.0 -> libz3.so.0.0.0*
-rwxr-xr-x. 1 root root 26743672 May 10 04:49 /usr/lib64/libz3.so.0.0.0*
fitzgen commented 4 years ago

Can you share the output of

$ ls -l /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib

? Thanks!

julian-seward1 commented 4 years ago

I don't have exactly that path, but I do have the same with lib64 at the end instead of lib. Anyways:

$ ls -l /home/sewardj/MOZ/WT/RMME/z3.rs/target/debug/build/z3-sys-5e134ff63c94fa4b/out/lib64
total 822460
drwxrwxr-x. 3 sewardj sewardj      4096 Oct 27 21:46 cmake/
-rw-r--r--. 1 sewardj sewardj 842187580 Oct 27 21:46 libz3.a
fitzgen commented 4 years ago

I don't have exactly that path, but I do have the same with lib64 at the end instead of lib.

Ah okay! This is definitely the source of the bug. I'll whip up a fix tomorrow.