`z3-sys` version `0.19.6` fails to build with `bundled` on arch

[gskorokhod]

The latest version of the crate (0.19.6) and the one before (0.19.5) fail to build with the bundled feature. The build is done inside an arch linux container.

Clang version is 21.1.6:

mayday@dev-box ~/Coding/conjure/conjure-oxide (gs248/misc *) > clang -v
clang version 21.1.6
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/bin
Found candidate GCC installation: /usr/bin/../lib/gcc/x86_64-pc-linux-gnu/15.2.1
Found candidate GCC installation: /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/15.2.1
Selected GCC installation: /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/15.2.1
Candidate multilib: .;@m64
Candidate multilib: 32;@m32
Selected multilib: .;@m64

The build error is:

...
Compiling z3-sys v0.10.3
error: failed to run custom build command for `z3-sys v0.10.3`
note: To improve backtraces for build dependencies, set the CARGO_PROFILE_DEV_BUILD_OVERRIDE_DEBUG=true environment variable to enable debug information generation.

Caused by:
  process didn't exit successfully: `/home/mayday/Coding/conjure/conjure-oxide/target/debug/build/z3-sys-e1c29077158cf782/build-script-build` (exit status: 101)
  --- stdout
  cargo:rerun-if-changed=build.rs
  downloading to /home/mayday/Coding/conjure/conjure-oxide/target/debug/build/z3-sys-d2b304c340be7b4f/out/z3

  --- stderr
  error: error decoding response body

  thread 'main' (267429) panicked at /home/mayday/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/z3-sys-0.10.3/build.rs:404:17:
  Could not get submodule asset for z3-sys-0.10.3
  stack backtrace:
     0: __rustc::rust_begin_unwind
               at /rustc/ed61e7d7e242494fb7057f2657300d9e77bb4fcb/library/std/src/panicking.rs:698:5
     1: core::panicking::panic_fmt
               at /rustc/ed61e7d7e242494fb7057f2657300d9e77bb4fcb/library/core/src/panicking.rs:75:14
     2: build_script_build::main
  note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Our Cargo.toml for the crate which links to z3-sys:

[package]
name = "conjure-cp-core"
version = "0.0.1"
edition = "2024"

[features]
default = []
smt = ["dep:z3"]
extra-rule-checks = []

[dependencies]
conjure-cp-rule-macros = { path = "../conjure-cp-rule-macros" }
conjure-cp-enum-compatibility-macro = { path = "../conjure-cp-enum-compatibility-macro" }
minion-sys = { path = "../minion-sys" }
tree-morph = { path = "../tree-morph" }
z3 = { version = "0.19.6", default-features = false, features = ["bundled"], optional = true }
uniplate = { workspace = true }
project-root = { workspace = true }
linkme = { workspace = true }
serde = { workspace = true }
serde_json = { workspace = true }
serde_with = { workspace = true }
strum = { workspace = true }
strum_macros = { workspace = true }
thiserror = { workspace = true }
log = { workspace = true }
tracing = { workspace = true }
tracing-subscriber = { workspace = true }
anyhow = { workspace = true }
regex = { workspace = true }
walkdir = { workspace = true }
derivative = { workspace = true }
schemars = { workspace = true }
clap = { workspace = true }
itertools = { workspace = true }
git-version = { workspace = true }
rustsat-minisat = { workspace = true }
rustsat = { workspace = true }
paste = { workspace = true }
static_assertions = { workspace = true }
defile = { workspace = true }
ustr = { workspace = true }
polyquine = { workspace = true }
syn = { workspace = true }
quote = { workspace = true }
proc-macro2 = { workspace = true }
num-traits = { workspace = true }

[dev-dependencies]
conjure-cp = { path = "../conjure-cp" }

[lints]
workspace = true

The build used to work before, but seems to be reliably failing now

[toolCHAINZ]

The relevant PRs would seem to be #472. Maybe this should be made into an optional feature flag. The error you're getting seems to be to be that the client that's reaching out to find the z3 git URL but the client itself is failing to make the request, presumably because of some incompatibility with that tls flag and arch systems?

We can look at changing this, but I do think that your suggestion in conjure-cp/conjure-oxide#1410 is probably the way to go for your use-case.

I would generally recommend using gh-release, which still statically links in z3, but that does limit you to platforms where z3 provides a binary release in their github releases.

If in your case you must build/statically link z3 for your targets (and z3 doesn't provide libs for them all), then bundling it yourself and using the flag you reference to link against it feels to me like a much more controllable way to get it done. If your builds are done in docker you could probably even avoid a submodule and just clone the repo/check out the tag/build in a Dockerfile.

[gskorokhod]

I would generally recommend using gh-release, which still statically links in z3, but that does limit you to platforms where z3 provides a binary release in their github releases.

Unfortunately it doesn't seem to have a pre-built release for my system

error: failed to run custom build command for `z3-sys v0.10.3`

Caused by:
  process didn't exit successfully: `/home/mayday/Coding/conjure/conjure-oxide/target/debug/build/z3-sys-2efd09942908b42a/build-script-build` (exit status: 101)
  --- stdout
  cargo:rerun-if-changed=build.rs
  cargo:rerun-if-env-changed=Z3_SYS_Z3_VERSION
  error: error decoding response body

  --- stderr

  thread 'main' (43987) panicked at /home/mayday/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/z3-sys-0.10.3/build.rs:140:17:
  Could not get release asset for z3-4.15.2 with os=glibc and arch=x64
  note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Although z3-4.15.2-x64-glibc-2.39.zip does seem to exist in https://github.com/Z3Prover/z3/releases so idk why it can't find it?

(I'm building in a distrobox container based on archlinux:latest... probably my fault for using a weird setup tbh)

In our CI it does seem to work but we've had other issues with GH rate limiting (and also whatever is going on in #476 - @lixitrixi would know more about that)

Either way, we've had some other issues with git rate limiting etc, so vendoring z3 is probably the way to go :)
Thanks!

[toolCHAINZ]

That's probably the same TLS error manifesting with a different error message (due to a different code-path in build.rs). The error decoding response body is probably coming from reqwest.

I've made and merged #486, which will soon be published to crates.io, which uses rustls-tls by default. This works in our CI as well as on my local machine and avoids these annoying non-rust build dependencies. When that's published, you might try that version and see if it works.

I've made the TLS provider configurable so it can be configured through a z3-sys feature flag in case someone really wants to use OpenSSL.

[toolCHAINZ]

This was published in 0.19.7

[daemontus]

Just FYI, I am running into the exact opposite situation on macOS. Everything works locally, but in CI, the build fails with a wrong HTTP status code returned when fetching either the bundled or gh-release Z3 (both produce the same behavior). So far I have not found a workaround yet, but I am now trying to switch back to vendor TLS, we'll see...

See here: https://github.com/sybila/biodivine-aeon-py/actions/runs/20824246013/job/59821093294

Edit: After a few experiments, the whole thing just feels utterly random... when building for Linux, rust-tls works, but not native-tls; when building for macOS, native-tls works but not rust-tls; when building with Conda on macOS, nothing works and I get 403 for every request... I understand that this is strictly speaking not your "fault", but any sort of guidance on how to deal with this would be welcome.

[toolCHAINZ]

@daemontus The 403 you're getting is almost certainly not because of rust-tls but because you're getting rate-limited by Github. Github does per-IP throttling on requests made over its API (which is what gh-release does). The reason it seems random is that your CI jobs are getting run on "randomly" allocated github CI runners, and some runners have hit the limit and some have not.

The way around this is to provision a read-only Github PAT and provision it to the CI job as I have done here:

z3.rs/.github/workflows/rust.yml

Line 178 in 11b153c

READ_ONLY_GITHUB_TOKEN: ${{ secrets.PUBLIC_REPO_TOKEN }}

The build.rs looks for READ_ONLY_GITHUB_TOKEN in the env and will use that token if it exists.

[daemontus]

Awesome, thank you! I will give it a try!