z3 soname bump

[Jerry James]

I will soon push a change to the z3 package, in Rawhide only, which
will result in an soname bump.  The actual contents of libz3 will not
change, however.  The only Fedora consumer outside of the z3 package
itself is cppcheck, which currently fails to build due to the recent
cmake change.  If the cppcheck maintainers want me to try to fix that,
I will do so; otherwise, I am happy to let them fix it themselves.

The gory details for those interested:

The z3 project has two build systems: an old one, based on generating
Makefiles with python scripts, and a new one based on cmake.  We have
been using the old one, because the cmake build system does not
support building z3's OCaml interface.  However, the old build system
has a number of ... features ... that we had to work around, leading
to a fair amount of uncleanness in the spec file.

I have decided to take the plunge and switch to using the cmake build
system, with manual steps afterward to build the OCaml interface.  The
old build system gave the z3 library an soname of "libz3.so", which
the spec file modified to be "libz3.so.0", with a versioned library
libz3.so.0.0.0.  The cmake build system gives the library an soname of
"libz3.so.4.8" (where 4 and 8 are the major and minor version numbers,
respectively), with a versioned library libz3.so.4.8.8.0.  This lets
me throw out a bunch of cruft, while introducing a much smaller amount
of cruft due to the OCaml interface.  I think it's a win.
-- 
Jerry James
http://www.jamezone.org/

[Jeff Law]

On Fri, 2020-07-24 at 13:15 -0600, Jerry James wrote:
>  I will soon push a change to the z3 package, in Rawhide only, which
>  will result in an soname bump.  The actual contents of libz3 will not
>  change, however.  The only Fedora consumer outside of the z3 package
>  itself is cppcheck, which currently fails to build due to the recent
>  cmake change.  If the cppcheck maintainers want me to try to fix that,
>  I will do so; otherwise, I am happy to let them fix it themselves.
>  
>  The gory details for those interested:
>  
>  The z3 project has two build systems: an old one, based on generating
>  Makefiles with python scripts, and a new one based on cmake.  We have
>  been using the old one, because the cmake build system does not
>  support building z3's OCaml interface.  However, the old build system
>  has a number of ... features ... that we had to work around, leading
>  to a fair amount of uncleanness in the spec file.
>  
>  I have decided to take the plunge and switch to using the cmake build
>  system, with manual steps afterward to build the OCaml interface.  The
>  old build system gave the z3 library an soname of "libz3.so", which
>  the spec file modified to be "libz3.so.0", with a versioned library
>  libz3.so.0.0.0.  The cmake build system gives the library an soname of
>  "libz3.so.4.8" (where 4 and 8 are the major and minor version numbers,
>  respectively), with a versioned library libz3.so.4.8.8.0.  This lets
>  me throw out a bunch of cruft, while introducing a much smaller amount
>  of cruft due to the OCaml interface.  I think it's a win. 
Just a note on z3.  

I've been trying to track down what I think is an uninstantiated template issue
that's exposed by LTO.  I've been chasing it on/off over the last day or two
without success.  So if you get a build failure that looks like this:

/usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x110): undefined reference to
`lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned int)
const'
/usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x168): undefined reference to
`lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned int)
const'
/usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x1b0): undefined reference to
`lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned int)
const'
collect2: error: ld returned 1 exit status

Just disable LTO via the usual mechanism (%define _lto_cflags %{nil}).  We'll
revisit any opt-outs again between F33 and F34 and re-evaluate them.

Jeff

[Jerry James]

On Fri, Jul 24, 2020 at 1:35 PM Jeff Law <law(a)redhat.com&gt; wrote:
>  Just a note on z3.
>
>  I've been trying to track down what I think is an uninstantiated template issue
>  that's exposed by LTO.  I've been chasing it on/off over the last day or two
>  without success.  So if you get a build failure that looks like this:
>
>  /usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x110): undefined reference to
> `lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned int)
> const'
>  /usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x168): undefined reference to
> `lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned int)
> const'
>  /usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x1b0): undefined reference to
> `lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned int)
> const'
>  collect2: error: ld returned 1 exit status
>
>  Just disable LTO via the usual mechanism (%define _lto_cflags %{nil}).  We'll
>  revisit any opt-outs again between F33 and F34 and re-evaluate them. 
Thanks for the heads-up, Jeff.  I have not seen that in a mock build,
but if there hasn't been a successful Rawhide compose since the LTO
bits landed, that is no surprise.  I have a vague memory of asking z3
upstream to add some explicit template instantiations around the time
gcc 10 landed in Rawhide, so there is precedent if we need to do so
again.

Regards,
-- 
Jerry James
http://www.jamezone.org/

[Jeff Law]

On Fri, 2020-07-24 at 13:39 -0600, Jerry James wrote:
>  On Fri, Jul 24, 2020 at 1:35 PM Jeff Law <law(a)redhat.com&gt;
> wrote:
>  > Just a note on z3.
>  > 
>  > I've been trying to track down what I think is an uninstantiated template issue
>  > that's exposed by LTO.  I've been chasing it on/off over the last day or
> two
>  > without success.  So if you get a build failure that looks like this:
>  > 
>  > /usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x110): undefined
> reference to `lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned
> int) const'
>  > /usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x168): undefined
> reference to `lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned
> int) const'
>  > /usr/bin/ld: /tmp/z3.16EntH.ltrans1.ltrans.o:(.data.rel.ro+0x1b0): undefined
> reference to `lp::lp_solver<double, double>::get_variable_name[abi:cxx11](unsigned
> int) const'
>  > collect2: error: ld returned 1 exit status
>  > 
>  > Just disable LTO via the usual mechanism (%define _lto_cflags %{nil}).  We'll
>  > revisit any opt-outs again between F33 and F34 and re-evaluate them.
>  
>  Thanks for the heads-up, Jeff.  I have not seen that in a mock build,
>  but if there hasn't been a successful Rawhide compose since the LTO
>  bits landed, that is no surprise.  I have a vague memory of asking z3
>  upstream to add some explicit template instantiations around the time
>  gcc 10 landed in Rawhide, so there is precedent if we need to do so
>  again. 
Whatever you committed in the last couple days seems to have fixed the
issue.  I
just got a clean build of z3 on x86_64.

jeff

[Jerry James]

On Mon, Jul 27, 2020 at 1:29 PM Jeff Law <law(a)redhat.com&gt; wrote:
>  Whatever you committed in the last couple days seems to have fixed
> the issue.  I
>  just got a clean build of z3 on x86_64. 
Hmmm.  That's mysterious.  All I did was switch us from building with
the old python script method to building with cmake.  I suppose it's
possible that different flags are passed to the compiler this way, but
the sources are exactly the same.
-- 
Jerry James
http://www.jamezone.org/

[Wolfgang Stoeggl]

Thanks Jerry for providing all the details about the z3 soname bump.
FYI: cppcheck has been rebuilt now [1]

Wolfgang

[1] https://koji.fedoraproject.org/koji/taskinfo?taskID=48648878