Stop ignoring errors in CI.

[waywardmonkeys]

No description provided.

[waywardmonkeys]

This PR is to see what happens in CI if we stop doing this...

[waywardmonkeys]

@SeeSpring I think you modified some of these lines last ... what do you think?

[SeeSpring]

Looks good. I think pinning sudo apt-get install libz3-dev to whatever version bindgen is generated against would also be useful to prevent missing symbols from occurring again.

This also reminds me that

z3.rs/z3/tests/lib.rs

Line 601 in 7d0f7e8

#[ignore = "See https://github.com/Z3Prover/z3/issues/5702"]

can be removed now.

[waywardmonkeys]

The problem with pinning libz3-dev is that in Ubuntu, only 4.8.12 is provided ... so if we stuck with that, we can't advance to current new features and fixes.

There are already a bunch of things that have been added with new APIs since 4.8.12 that might be good to support ...

If we used GitHub Actions cache action support, we could reduce the cost of doing the Z3 compilation and make it more reasonable to always build our own Z3 by default ...

[SeeSpring]

If we don't pin, then if a user uses the z3 crate on Ubuntu with static-link-z3 off, they might end up getting linking errors despite CI passing. Forcing users to use static linking feels unreasonable with how long the build times are (~15 minutes)

I think it boils down to synchronizing the API that z3-sys builds against with the API of the system version of z3.

Do you know how other -sys crates handle a changing C API?

[waywardmonkeys]

Not offhand yet.

There are a variety of issues here ... one is that the enumerations in the past weren't always updated in a consistent way from release to release of Z3, so sometimes values got re-used or re-ordered.

I've also started looking at Z3 itself to see if perhaps the compilation could be faster.

[SeeSpring]

At least in CI, it seems that

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

Lines 61 to 64 in bb57297

	- name: Build z3-sys with statically linked Z3
	run: cargo build --manifest-path z3-sys/Cargo.toml -vv --features static-link-z3
	- name: Build z3 with statically linked Z3
	run: cargo build --manifest-path z3/Cargo.toml -vv --features static-link-z3

results in compiling z3 twice. I'm not sure how to fix it though

[waywardmonkeys]

I'm not sure how to fix it though

I'm not sure that we need to test building each one separately. Just doing a cargo build -vv --features static-link-z3 once should be fine...