Use system-shipped z3 libraries by pkg_config

prove-rs / z3.rs

Rust bindings for the Z3 solver.

347 stars 110 forks source link

Use system-shipped z3 libraries by pkg_config #248

Closed wtdcode closed 11 months ago

wtdcode commented 1 year ago

Probably a bit more elegant way to use precompiled binaries compared to #193 by utilizing pkg-config, which is ubiquitous of all *nix platforms.

My usecase is to use homebrew installed z3 library.

Changes:

Detect dynamic/static precompiled libraries and use them with pkg_config
Add CI for macos using precompile libraries from homebrew.
Instead of manually encoded z3/src/api/z3.h, use the universal z3.h with corresponding include directories added, which should be a more general approach.

No break changes are introduced in theory and should be safe to go.

waywardmonkeys commented 1 year ago

There is also now #249 which differs some from this ...

wtdcode commented 1 year ago

There is also now #249 which differs some from this ...

It’s totally different because it will use dynamic libraries from distributions like homebrew, Debian etc. In other words, the two PRs are not conflicting regarding features offered.

waywardmonkeys commented 1 year ago

Okay, so now we have vcpkg support. What scenarios does having this help us in? We already build out of the box with syste, provided z3 on macOS (via homebrew) and with the Ubuntu package. Is it that you could build your own and have it elsewhere?

wtdcode commented 1 year ago

Okay, so now we have vcpkg support. What scenarios does having this help us in? We already build out of the box with syste, provided z3 on macOS (via homebrew) and with the Ubuntu package. Is it that you could build your own and have it elsewhere?

I can't understand how vcpkg helps here.

poscat0x04 commented 1 year ago

Can confirm this works on fedora without manually setting the environment variable!

poscat0x04 commented 1 year ago

@waywardmonkeys The problem is that bindgen is not finding the header files when it should be because the include path is not set up correctly. Most linux distributions use pkg-config to specify C library metadata such as include path, linker flags etc.

poscat0x04 commented 1 year ago

I've fixed the merge conflict, here is a patch: resolve-conflict.patch

waywardmonkeys commented 1 year ago

I will get this landed later today when I am back home.

poscat0x04 commented 11 months ago

politely pings @waywardmonkeys

waywardmonkeys commented 11 months ago

I've done a fresh update of this PR in #277 and will land it once it passes CI.

Thanks for the initial work!