prove-rs / z3.rs

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

New release #294

Open toolCHAINZ opened 3 months ago

toolCHAINZ commented 3 months ago

I noticed it's been a while since a new version of these bindings have been pushed to crates.io and there's some really good stuff missing from that version.

Any possibility of a release in the near future?

waywardmonkeys commented 3 months ago

I'd like to ... I want to get the bundled Z3 updated, but that is still failing and I need to figure out the right fix. Just now in fixing something else, the WebAssembly build failed due to an error in Z3 and I've just submitted a PR for that. (That will require a new release of Z3...)

Would be good to do though!

toolCHAINZ commented 3 months ago

Gotcha, thanks! Please let me know if there's any way I can help out; I've loved using this library and wouldn't mind contributing if there was something I could do. Out of curiousity, what is failing? I just pulled down z3.rs and bumped z3-sys/z3 to z3-4.13.0 and all the z3-sys and z3 tests passed (ARM macOS).

Ohhhh, I see the failed Windows builds...

toolCHAINZ commented 3 months ago

Poking around at this a bit on my Windows 11 machine (apologies if you've already triaged all this):

It looks like for some reason the debug build is emitting a linker flag to link to msvcrt.lib, which is the release version of the library. But there seems to be a default link to the debug version of the same library?

  = note: LINK : warning LNK4098: defaultlib 'MSVCRTD' conflicts with use of other libs; use /NODEFAULTLIB:library

I'm guessing the default linker flags for the release profile link to msvcrt.lib, so it just ends up being a duplicated flag instead of a conflicting flag.

waywardmonkeys commented 3 months ago

I know that it is from doing debug builds on Windows, but not much beyond that. I haven't been booting my Windows machine often as of late ... I also know that it started when I increased the cmake version requirements in upstream Z3 (and therefore being subject to changes in the cmake policies).

toolCHAINZ commented 3 months ago

Ok, I just tracked down some cmake stuff. Bisected cmake versions and it seems that 3.15 is the first version breaking the debug tests.

Still looking through the changelog for that version, but the following item does pop out:

The CMAKE_MSVC_RUNTIME_LIBRARY variable and MSVC_RUNTIME_LIBRARY target property were introduced to select the runtime library used by compilers targeting the MSVC ABI. See policy CMP0091.

toolCHAINZ commented 3 months ago

Not at all a CMake expert here, but I'm wondering if this is a cmake-rs problem

This snippet seems to indicate that cmake-rs is attempting to communicate /MT and /MD type flags through CMAKE_{LANG}_FLAGS_{CONFIG} variables:

https://github.com/rust-lang/cmake-rs/blob/c4a60dd154dd90e469dffc41a1faa717704f90b3/src/lib.rs#L731-L754

But CMP0091 seems to indicate that MSVC lib selection is no longer done through these flags. So maybe cmake-rs is using a deprecated flag, cmake is ignoring it, and that's causing the mismatch.

toolCHAINZ commented 3 months ago

I've made https://github.com/prove-rs/z3.rs/pull/295 which contains a change that fixes debug builds on my machine.