Cannot build with Z3 4.8.5
ocharles opened this issue · 6 comments
Preprocessing library for z3-408.0..
Building library for z3-408.0..
[1 of 4] Compiling Z3.Base.C ( dist/build/Z3/Base/C.hs, dist/build/Z3/Base/C.o )
[2 of 4] Compiling Z3.Base ( src/Z3/Base.hs, dist/build/Z3/Base.o )
[3 of 4] Compiling Z3.Opts ( src/Z3/Opts.hs, dist/build/Z3/Opts.o )
[4 of 4] Compiling Z3.Monad ( src/Z3/Monad.hs, dist/build/Z3/Monad.o )
[1 of 4] Compiling Z3.Base.C ( dist/build/Z3/Base/C.hs, dist/build/Z3/Base/C.p_o )
[2 of 4] Compiling Z3.Base ( src/Z3/Base.hs, dist/build/Z3/Base.p_o )
[3 of 4] Compiling Z3.Opts ( src/Z3/Opts.hs, dist/build/Z3/Opts.p_o )
[4 of 4] Compiling Z3.Monad ( src/Z3/Monad.hs, dist/build/Z3/Monad.p_o )
Preprocessing test suite 'spec' for z3-408.0..
Building test suite 'spec' for z3-408.0..
[1 of 2] Compiling Z3.Base.Spec ( test/Z3/Base/Spec.hs, dist/build/spec/spec-tmp/Z3/Base/Spec.o )
[2 of 2] Compiling Main ( test/Spec.hs, dist/build/spec/spec-tmp/Main.o )
Linking dist/build/spec/spec ...
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: dist/build/spec/spec-tmp/Z3/Base/Spec.o: in function `c8YP_info':
(.text.s8Ln_info+0x278): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o):(.text.zz3zm408zi0zm7xF7S34UzzMR9jLZZteoIWY7_ZZ3ziBase_zdwmkIntSort_info+0x9c): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o): in function `c191G_info':
(.text.s10Eu_info+0x240): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o): in function `c195Q_info':
(.text.zz3zm408zi0zm7xF7S34UzzMR9jLZZteoIWY7_ZZ3ziBase_zdwmkTrue_info+0x14d): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o): in function `c197F_info':
(.text.zz3zm408zi0zm7xF7S34UzzMR9jLZZteoIWY7_ZZ3ziBase_zdwmkFalse_info+0x14d): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o):(.text.s10LJ_info+0x280): more undefined references to `Z3_get_error_msg_ex' follow
Git HEAD tests fail though, and somewhat mysteriously at that:
Running 1 test suites...
Test suite spec: RUNNING...
Test suite spec: FAIL
Test suite logged to: dist/test/z3-408.0-spec.log
0 of 1 test suites (0 of 1 test cases) passed.
$ cat haskell-z3-009772a/dist/test/z3-408.0-spec.log
Test suite spec: RUNNING...
Test suite spec: FAIL
Test suite logged to: dist/test/z3-408.0-spec.log
🤷♂️
Hi, yes, I can make a release relatively soon (this weekend or the next).
For the record, I just do my best to keep this library alive. The library seems to have a decent number of users but none of them really wants to help maintaining it. Most I can do is to guide those who want to contribute, review and merge pull requests.
@IagoAbal I'm happy to help maintain, but I don't really know anything about Z3 - I just use this library via SBV. If you want another person to help cut releases though, I'm happy to help there.
Supposedly fixed by b8ce65d, please reopen if that is not the case.
I just use this library via SBV
That cannot be the case, SBV does not use these bindings as far as I can tell. SBV talks to Z3 via its SMT-LIB front-end. Correct me if I'm wrong.
You are absolutely correct. In that case I have no idea what depends on z3 in our codebase... but something does! 😄