Build failure for gh-release crates.io dependency

[lixitrixi]

We've been experiencing a few issues in CI that seem to be caused by the gh-release feature and crates.io dependency.

1. The feature seems to be inexplicably messing with our import of an internal macro crate which does not depend on z3. Changing to bundled resolved this for us.

• See Failed compilation due to missing conjure_cp_essence_macros crate conjure-cp/conjure-oxide#1327. The first broken commit was the one which changed from a git dependency to a gh-release crates.io dependency, in refactor: depend on z3 from crates.io conjure-cp/conjure-oxide#1304.

2. When updating to 0.19.5 with gh-release we get the following error in all build environments.

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

Caused by:
  process didn't exit successfully: `/home/runner/work/conjure-oxide/conjure-oxide/target/debug/build/z3-sys-6814f68fac856a2c/build-script-build` (exit status: 101)
  --- stdout
  cargo:rerun-if-changed=build.rs
  cargo:rerun-if-env-changed=Z3_SYS_Z3_VERSION

  --- stderr

  thread 'main' (30329) panicked at /home/runner/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/z3-sys-0.10.3/build.rs:197:9:
  assertion `left == right` failed
    left: 401
   right: 200

It seems that these two issues are related since using bundled fixes both, but in the former case there could be a silent error during compilation which messes with the macro crate? I expect this has something to do with rate limiting as mentioned in conjure-cp/conjure-oxide#1306, but we addressed that with tokens (as far as I understand, but I wasn't involved directly).

[lixitrixi]

I will take a deeper look at this when I have some time, with more verbose logs to try and catch any silent errors.

[toolCHAINZ]

My response might be a little fragmented as there seems to be a few things going on here.

For the 401 response for 0.19.5, I'm fairly sure this is because the PR you link was opened by dependabot. It looks like dependabot has a separate secret managment setup in github. Under the repo's settings see there's a "dependabot" section under Secrets and Variables. My guess is that the repo isn't providing the token to the job since dependabot opened it, it's sending an empty "token" and GH is returning a 401 since it's not a real token.

[toolCHAINZ]

My only theory for the other error is that both build.rs stages and macro crate compilations happen early in the compilation pipeline, before the main sources are compiled. Maybe if there was some build issue in z3-rs, it terminated this early stage, interfering with the production of artifacts for the macro crate, causing that strange error?

I would have expected to see an error coming out of z3's build.rs though, which I don't see in that issue. We build z3 on x86 in docker with gh-release in our CI so I'm not sure exactly what could be going wrong there; I don't see anything in the conjure docker build environment that I would think would prevent building...

You mentioned you had build issues on your x86 machine, right @lixitrixi? Do you have any more detail on what is failing? Does it fail if you run cargo clean and then build again?

[toolCHAINZ]

Oh wait, I think I might know what's going on.

Were the failed docker builds targeting 0.19.4? 0.19.4 uses rust's tls bindings, but requires the dev headers for openssl to be installed. These aren't installed by default in ubuntu I think.

0.19.5 includes #472 which uses a vendored ssl library, removing this requirement (and making it usable in a minimal docker image without apt installing more stuff).

If you make the upgrade to 0.19.5, I'd be curious to know if that allows it to build on your machine. Though I'm still puzzled why gh-release would break then but bundled would not...

Out of curiousity, what's the method of distribution for your project? If users are going to be always running it in a docker container, it may make more sense to just install an up-to-date Z3 in your dockerfile, not use bundled or gh-release and sidestep all of this.

[lixitrixi]

You mentioned you had build issues on your x86 machine, right @lixitrixi? Do you have any more detail on what is failing? Does it fail if you run cargo clean and then build again?

Yes, it seemed to be downloading everything alright but the actual binding was failing due to some missing symbols. It looks like my local C++ standard library is out of date, and I've given up on trying to update it and just stuck with using bundled locally since I'm on a time crunch :)

I tried updating to 0.19.5, unfortunately it still fails with the same errors like below:

Undefined symbols for architecture x86_64:
            "std::__1::basic_filebuf<char, std::__1::char_traits<char>>::close()", referenced from:
                ast_manager::~ast_manager() in libz3_sys-f5e38c42f3d5f620.rlib(ast.o)

Out of curiousity, what's the method of distribution for your project?

We're trying to include solvers with the compiled binary, so unfortunately relying on a locally installed Z3 won't work :/

[toolCHAINZ]

Hmmm your link issues sound quite puzzling haha. Maybe it's that z3 is releasing binaries dynamically linked to llvm libc and your system is using GNU? Unfortunately somewhat outside my experience. @lmondada any thoughts?

Have you seen linking errors similar to that in CI?

The error conditions I'm tracking here are:

• Your local libc linking issue
• An unspecified CI error?
• The mysterious macro crate error (which as far as I can tell is outside CI?)

Does that capture it all?

[lixitrixi]

I'm honestly alright with the linking issue, since it doesn't appear in CI and I can easily avoid it by using bundled. It seems to affect only me, and I'm on a relatively old machine anyways. If there's a quick fix for it though I'd appreciate it!

We'll see if dependabot's secret fixes the problem with updating, but I have no idea about the macro crate build error. I remember briefly seeing a one-off 403 error (instead of 401) in CI while developing. I'm now wondering if that could be relevant...

[toolCHAINZ]

A 403 is probably relevant. Hopefully we can eventually get this all tracked down and smoothed out for future users haha. Thanks for your patience!

[lixitrixi]

Giving Dependabot its own secret worked and let us update to 0.19.5, thank you!

We're still getting some OpenSSL errors in our docker environment that make it tricky to reproduce the macro crate build failure, see conjure-cp/conjure-oxide#1327 (comment). We'll see if we can resolve this and the failure stays.

[toolCHAINZ]

Strange. Maybe it's worth seeing if we can make reqwest use rustls instead? Or maybe we allow configuring through a feature flag?

[lmondada]

Hey both,

Unfortunately I don't think I am of much help either. @lixitrixi if you are distributing pre-compiled binaries and want z3 statically linked in, you might be better off pinning a version of z3 and having a copy of the libraries for the supported platforms in your repo?

It's a bit more maintenance, but that will keep your builds self-contained rather than always fetching it over the internet.

@toolCHAINZ the way I've implemented this feature seems to regularly create issues... I'll have a think to see if I can think of a more robust solution