delcypher added a comment. In D54978#1431788 <https://reviews.llvm.org/D54978#1431788>, @ddcc wrote:
> The only relevant commit that I can find is > https://github.com/Z3Prover/z3/commit/2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979 > , but it first landed in z3 4.6.0. It looks like it's specific to CMake > though, so is it different if you use the python build? I haven't tried the > CMake build. Hmm this looks like there are some bugs in the different Z3 build systems. So for the CMake build the value of `Z3_FULL_VERSION_STR` is used to populate the `Z3_FULL_VERSION` macro in the header file. Initially this is `"${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}"` but then If the git has is available we append to it https://github.com/Z3Prover/z3/blob/c0f7afacc497e7e2e1a2a28bcebf1173933f5bab/CMakeLists.txt#L96 and if the git description is available we append to it https://github.com/Z3Prover/z3/blob/c0f7afacc497e7e2e1a2a28bcebf1173933f5bab/CMakeLists.txt#L109 This was my attempt at mimicking the `get_full_version_string()` function ( https://github.com/Z3Prover/z3/blob/038f992ff485d0bf93f962dc9e45330ff1e2e47d/scripts/mk_util.py#L3065 ) when I added Z3's CMake build system. Unfortunately this doesn't quite match what Z3's python build system does. - In the python build system the `VER_REVISION` global (used to set `Z3_REVISION_NUMBER` macro and is the forth integer in `Z3_FULL_VERSION`, i.e. `d` in `a.b.c.d`) tries to count the number of commits reachable from the current git `HEAD` (see https://github.com/Z3Prover/z3/blob/038f992ff485d0bf93f962dc9e45330ff1e2e47d/scripts/mk_util.py#L561 ). The CMake build system doesn't mimic this. Personally I don't think the python build system makes sense here at all given that this integer goes in the 4th position in the version output (i.e. `d` in `a.b.c.d`). - In the CMake build system the 4th integer in `Z3_FULL_VERSION` is always whatever `Z3_VERSION_TWEAK` is set to in the root `CMakeLists.txt` file. So far, I think has always been `0`. So the bug here is that the CMake and python build systems don't agree on the meaning of the 4th version field. Personally I think the implementation of Z3's CMake build system makes more sense given where it is placed in the version string but that means the name `Z3_REVISION_NUMBER` macro name isn't very appropriate. None of this really mattered until the version header file became public Would one of you be able to file a bug against Z3 to fix this? I am no longer in a position to contribute to Z3 so I can't do this. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
