Bad `.dylib` versioning in `pip` package.

[zwimer]

The .dylib distributed in the pip package of z3 seems to have bad version info in it. Here is a comparison of the version distributed through homebrew vs pip. Notice the pip version lists versions as 0.0.0.

From pip:

$ otool -L libz3.4.12.dylib
libz3.4.12.dylib:
    libz3.dylib (compatibility version 0.0.0, current version 0.0.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1311.0.0)
    /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1200.3.0)

From homebrew:

$ otool -L libz3.4.12.dylib
libz3.4.12.dylib:
    /opt/homebrew/opt/z3/lib/libz3.4.12.dylib (compatibility version 4.12.0, current version 4.12.1)
    /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.32.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)

[NikolajBjorner]

12.0 vs 12.1 will be resolved in next release

[zwimer]

@NikolajBjorner For clarification, are you saying this libz3.dylib (compatibility version 0.0.0, current version 0.0.0) issue happens only on 12.0; and that the z3-solver==4.12.1.0 release is distributing the 12.0 library, but this will be fixed on the next release?

The python version installed that has the error above is z3-solver==4.12.1.0.

[NikolajBjorner]

the version discrepancy between 12.0 and 12.1 should be fixed. There were two releases after each other to fix a local problem. I don't know about what is the cause of version 0.0.0 showing up and will not be able to address it on my own.

[zwimer]

@NikolajBjorner I'm not sure what the 12.0 and 12.1 discrepancy is; both my pip and brew installs are 12.1. This issue was meant to be about this:

I don't know about what is the cause of version 0.0.0 showing up and will not be able to address it on my own.

That is the issue I meant to bring to light in this issue. I can re-word the issue above to make this more clear if it was unclear before, but given the issue is still present I think it should be re-opened (I am assuming it was closed due to a misunderstanding, please correct me if I am mistaken).

[NikolajBjorner]

what is the fix?

[zwimer]

what is the fix?

I'm not sure what is causing the 0.0.0 version issue; it is only on the pip build not the homebrew build, so it might be evident in the difference in cmake flags passed during the build step.

What I meant to say was that it might be useful to re-open this issue until the 0.0.0 issue earlier is resolved and add a 'Help Wanted' label to this issue? Either that or open then re-close the issue as "won't fix" if there is no intention to fix this nor be open to PRs for it.

With that in mind, if my initial wording was confusing somehow, please let me know how and I'll edit the initial post (or create a new issue if you prefer) for this 0.0.0 bug.

[zwimer]

@NikolajBjorner Just making sure this wasn't forgotten. Should this issue be:

1. Reopened as the issue still presists
2. A new issue made linking this
3. Labeled as a "won't fix"? (github has a special close option for these issues)

Unless I misunderstood, this issue was closed as the issue was misunderstood (perhaps my original description of the problem was unclear? I can edit it if you let me know what part was confusing). Thanks!

[NikolajBjorner]

Does anybody know how to fix this?

[NikolajBjorner]

the pip package binaries is still built using mk_unix_dist.py, which uses mk_util.py. It does not set -compatibility_version nor -current_version in the linker flags. The homebrew binaries you look at are probably built using the cmake build system. We can fiddle with scripts/mk_util.py to set the compatibility and current versions. It is easier for a mac user to test: build dylib using the python build system, check if these settings are in the dll (expected they are not), then add link flags to the appropriate MacOS ldflags in mk_util.py and check that they are set. Then add pull request.

[waywardmonkeys]

Could we have pip use make to do the build instead of the other build system?