prove-rs / z3.rs

Rust bindings for the Z3 solver.
331 stars 104 forks source link

Can't link application that depends on z3-sys built with feature vcpkg on Linux #257

Closed hermanventer closed 9 months ago

hermanventer commented 9 months ago

This seems to be a known issue, since the build_with_vcpkg_installed_z3 Github workflow job only adds Windows to the matrix (for my use case, at least, macos works).

The failure I see when building MIRAI on Linux (in a Github action) includes this bit:

error: linking with `cc` failed: exit status: 1
  |
  = note: /usr/bin/ld: /home/runner/work/MIRAI/MIRAI/vcpkg/installed/x64-linux/lib/libz3.a(api_arith.cpp.o): in function `_GLOBAL__sub_I_api_arith.cpp':
          api_arith.cpp:(.text.startup+0x10): undefined reference to `std::ios_base::Init::Init()'
          /usr/bin/ld: api_arith.cpp:(.text.startup+0x17): undefined reference to `std::ios_base::Init::~Init()'
          /usr/bin/ld: /home/runner/work/MIRAI/MIRAI/vcpkg/installed/x64-linux/lib/libz3.a(api_ast.cpp.o): in function 

Making an actual issue for this to track it separately from comment threads in PRs.

waywardmonkeys commented 9 months ago

This looks like it isn't linking in the C++ standard library. We have custom code in the cmake code path to handle this (although this should happen somewhere else probably). I guess we'll need similar for vcpkg as well ...

waywardmonkeys commented 9 months ago

The vcpkg build isn't enabled on Linux as it doesn't seem like GitHub had it available there or we have to do something different from what we're doing now...

waywardmonkeys commented 9 months ago

Yes, doing a quick PR that tries to enable vcpkg on macOS (#258) shows that we need to link the C++ library there as well.

I'll fix that later today as part of #258.

waywardmonkeys commented 9 months ago

The problem with the C++ stdlib is on master via 33b139d92817b51090aba5d094aaa114c74e2bba now.

This was done in PR #258 which also added macOS and Linux vcpkg builds to CI.