search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Rename `static-link-z3` to `bundled`. #260

Closed waywardmonkeys closed 10 months ago

waywardmonkeys commented 10 months ago

This renames the static-link-z3 build feature to bundled but leaves a bit around for now to maintain compatibility.

It also improves the README's discussion a little bit to mention vcpkg.

waywardmonkeys commented 10 months ago

FYI @TheVeryDarkness @hermanventer @Pat-Lafon @yasuo-ozu @wtdcode

This lays the ground for starting to use pkg-config to find the system-provided build (#248) and downloading pre-built Z3 binaries (#249).

TheVeryDarkness commented 10 months ago

How about uploading the z3 built by vcpkg? It's statically linked. Then we can download it.

waywardmonkeys commented 10 months ago

@TheVeryDarkness The Rust binary ABI isn't stable, so it would be specific to a particular version or set of versions of Rust. But getting #249 in place with downloading the Z3 binary might be good for what you want?

TheVeryDarkness commented 10 months ago

@TheVeryDarkness The Rust binary ABI isn't stable, so it would be specific to a particular version or set of versions of Rust. But getting #249 in place with downloading the Z3 binary might be good for what you want?

A question I've met with the binary downloaded from z3 release is that it seems to be dynamically linked. In rust, it's not recommended, and in my test cases, doctests might fail, as dynamic library may not be found, And distributing our program with a .dylib or a .dll may be a little annoying.

As far as I know, vcpkg is building z3 as a cpp project, therefore it's following cpp ABI. Maybe let me have a try. I'm already testing uploading and downloading our built z3.

Thanks for your answer.

waywardmonkeys commented 10 months ago

Ah, just the libz3.a ... not the z3-sys or z3 crate outputs ...

TheVeryDarkness commented 10 months ago

Ah, just the libz3.a ... not the z3-sys or z3 crate outputs ...

Yep. Sorry, I didn't make it clear.

TheVeryDarkness commented 10 months ago

Anyway, we can provide a lot of options.

Pat-Lafon commented 10 months ago

Is it possible to add a compile-time warning from build.rs if it is built with the static-link-z3 flag?

TheVeryDarkness commented 10 months ago

@TheVeryDarkness The Rust binary ABI isn't stable, so it would be specific to a particular version or set of versions of Rust. But getting #249 in place with downloading the Z3 binary might be good for what you want?

I think #249 is good enough if users are just using z3 for their own usage. Is there anything preventing it from being in place?

Days ago, I opened an issue in z3 repository, asking whether they can build a statically-linked one, but got a refusal.

TheVeryDarkness commented 10 months ago

Is it possible to add a compile-time warning from build.rs if it is built with the static-link-z3 flag?

Maybe a println! or eprintln!?

waywardmonkeys commented 10 months ago

Warning added:

$ cargo build --features static-link-z3
   Compiling z3-sys v0.8.1 (... z3-sys)
warning: The 'static-link-z3' feature is deprecated. Please use the 'bundled' feature.
   Compiling z3 v0.12.1 (... z3)
    Finished dev [unoptimized + debuginfo] target(s) in 1m 37s