Bug#830569: RFS: z3/4.4.1-0.1 [NMU] [4xRC]
Package: sponsorship-requests Severity: important Dear mentors, I am looking for a sponsor for a NMU of the z3 package. The update attempts to fix four RC bugs currently reported for z3. Changes since the last upload: * New upstream release. * Remove patches that were fixed upstream: - signed_char01 - signed_char02 - signed_char03 - signed_char04 - disable_test - disable_test2 - disable_test3 - disable_test4 (upstream issue has been closed: https://github.com/Z3Prover/z3/issues/210) - fix_conflict * Migrate remaining patches to DEP-3 format. * Rewrite typos.patch to apply to new version of z3. * Add patch fix-dotnet-version.patch (Closes: #808695). * Upgrade to Standards version 3.9.8 (no changes). * Install shared libraries into new libz3-4 package (Closes: #819884). * Install python files directly into /usr/lib/python2.7/dist-packages/ (Closes: #802272). * Clean up debian/rules. * Remove unnecessary version restriction of build dependency cli-common-dev. * Format debian/control with cme. * Fix debian/copyright: Change MIT to Expat and move Expat license text into separate license block so that it covers both file blocks. * Move libz3-ocaml-dev into section ocaml. * Add preinst scripts to remove directories from older versions to allow debhelper to install symlinks (Closes: #823573). * Disable tests as they fail eventually. As for the Lintian warnings: I've tried building z3 with hardening flags turned on, but the build failed. I don't know what the problem with the -dev package is; contrary to what Lintian claims, it *does* contain a symlink to the respective shared library. There are a few other issues that I was not able to fix, but I think closing the four RC bugs has a higher priority right now. The package is available on Mentors: https://mentors.debian.net/package/z3 dget -x https://mentors.debian.net/debian/pool/main/z/z3/z3_4.4.1-0.1.dsc Regards, Fabian Wolff
Bug#830569: RFS: z3/4.4.1-0.1 [NMU] [4xRC]
Hi Fabian!
I don't intend to sponsor this upload, but here's a quick review:
* Fabian Wolff , 2016-07-09, 16:14:
* Add patch fix-dotnet-version.patch (Closes: #808695).
This gives me no clue what the patch is about.
* Upgrade to Standards version 3.9.8 (no changes).
I don't think this is a good idea for an NMU.
* Install shared libraries into new libz3-4 package (Closes: #819884).
Now that the -dev package doesn't ship any ELFs, you should remove
${shlib:Depends} from -dev's Depends.
"Pre-Depends: ${misc:Pre-Depends}" should be moved to the shared library
package, or removed completely, because it's not needed these days.
* Install python files directly into /usr/lib/python2.7/dist-packages/
AFAICS, upstream build system installs these files in the right place,
so there should be no need to pick the *.py files from src/.
These d/rules lines are effectively no-ops and should be removed:
mkdir -p debian/tmp/usr/lib/python2.7/dist-packages/z3
touch debian/tmp/usr/lib/python2.7/dist-packages/z3/__init__.py
(The latter is probably a failed attempt of fixing #791604, which looks
like a previous incarnation #819884.)
* Remove unnecessary version restriction of build dependency
cli-common-dev.
Hmm, I don't know anything about CLI, but dh_cligacpolicy disagrees:
dh_cligacpolicy: Warning! No Build-Depends(-Indep) on cli-common-dev (>= 0.5.7)!
* Format debian/control with cme.
I don't think cosmetic changes are good idea for an NMU.
* Disable tests as they fail eventually.
All the tests? :-O
I've tried building z3 with hardening flags turned on, but the build
failed.
What was the error message?
I don't know what the problem with the -dev package is; contrary to
what Lintian claims, it *does* contain a symlink to the respective
shared library.
Yes, it does look like a bug in Lintian. Apparently it gets confused by
the -ocaml-dev package:
$ lintian libz3-4_4.4.1-0.1_amd64.deb libz3-dev_4.4.1-0.1_amd64.deb
[nothing]
$ lintian libz3-4_4.4.1-0.1_amd64.deb libz3-dev_4.4.1-0.1_amd64.deb
libz3-ocaml-dev_4.4.1-0.1_amd64.deb
W: libz3-4: dev-pkg-without-shlib-symlink usr/lib/x86_64-linux-gnu/libz3.so.4
usr/lib/x86_64-linux-gnu/libz3.so
W: libz3-ocaml-dev: hardening-no-relro usr/lib/ocaml/z3/dllz3ml.so
There are a few other issues that I was not able to fix, but I think
closing the four RC bugs has a higher priority right now.
Absolutely. It's not NMUer obligation to fix every known bug.
--
Jakub Wilk
Bug#830569: RFS: z3/4.4.1-0.1 [NMU] [4xRC]
Control: tags -1 + moreinfo * Jakub Wilk , 2016-07-09, 20:33: Yes, it does look like a bug in Lintian. Apparently it gets confused by the -ocaml-dev package: $ lintian libz3-4_4.4.1-0.1_amd64.deb libz3-dev_4.4.1-0.1_amd64.deb [nothing] $ lintian libz3-4_4.4.1-0.1_amd64.deb libz3-dev_4.4.1-0.1_amd64.deb libz3-ocaml-dev_4.4.1-0.1_amd64.deb W: libz3-4: dev-pkg-without-shlib-symlink usr/lib/x86_64-linux-gnu/libz3.so.4 usr/lib/x86_64-linux-gnu/libz3.so Actually, the culprit is that libz3-dev must depend libz3-4, but it doesn't. (OTOH, libz3-ocaml-dev does depend on libz3-4, which tricked Lintian into thinking this is where the .so symlink should be.) -- Jakub Wilk
Bug#830569: RFS: z3/4.4.1-0.1 [NMU] [4xRC]
Hi (please cc the bug) >I removed it, but does it do any harm? no, I guess not >Might have something to do with -fPIE vs. -fPIC, but one would have to >investigate further to be sure. This is definitely not a regression, >though, since the z3 version currently in the archive has no hardening >flags enabled, either. you are building a library, so I think you should use PIC for library, and PIE for binary. >I have reuploaded the fixed version to Mentors: seems better, but e.g. it lacks of breaks+replaces, because you moved files between the dev package and the new shiny one you introduced https://wiki.debian.org/PackageTransition at least I would expect to forward upstream failing tests --- z3-4.4.0/examples/python/hamiltonian/hamiltonian.py 2015-06-17 21:48:28.0 +0200 +++ z3-4.4.1/examples/python/hamiltonian/hamiltonian.py 2016-07-10 00:23:47.0 +0200 @@ -1,5 +1,5 @@ -# Copyright (c) 2012 Ganesh Gopalakrishnan gan...@cs.utah.edu +# Copyright (c) Microsoft Corporation. All Rights Reserved. please fix debian/copyright other stuff LGTM G.
Bug#830569: RFS: z3/4.4.1-0.1 [NMU] [4xRC]
Any reason why your .orig.tar is different than the one uscan downloads?
$ md5sum z3_4.4.1.orig.tar.gz*
94e21f86056f986c320653912be53f8a z3_4.4.1.orig.tar.gz
4336a9df24f090e711c6d42fd4e2b1fc z3_4.4.1.orig.tar.gz.github
* Fabian Wolff , 2016-07-10, 00:56:
* Install shared libraries into new libz3-4 package (Closes: #819884).
Now that the -dev package doesn't ship any ELFs, you should remove
${shlib:Depends} from -dev's Depends.
"Pre-Depends: ${misc:Pre-Depends}" should be moved to the shared
library package, or removed completely, because it's not needed these
days.
I removed it, but does it do any harm?
They didn't have any effect on the binary package. They were just
misleading.
These d/rules lines are effectively no-ops and should be removed:
mkdir -p debian/tmp/usr/lib/python2.7/dist-packages/z3
touch debian/tmp/usr/lib/python2.7/dist-packages/z3/__init__.py
(The latter is probably a failed attempt of fixing #791604, which
looks like a previous incarnation #819884.)
True, I fixed it. The first mkdir is necessary, though, to make the
directory debian/tmp/usr/lib/python2.7/dist-packages/. dh_auto_install
fails otherwise.
It would be cool to fix the upstream build system, so that it creates
dist-packages when it's missing.
* Disable tests as they fail eventually.
All the tests? :-O
It's more like one big one that calls individual functions that test
something. Most of the tests passed, but after about 1 GB (!) of test
output had been written on screen, something segfaulted. This is one of
those issues that probably need further investigation,
To be frank, I don't thin disabling whole testsuite is a good plan,
especially for an NMU. The package might mostly work for you, but maybe
it'll be completely broken when compiled on another architecture or with
a different compiler version. We do want to notice when this happens.
I've tried building z3 with hardening flags turned on, but the build
failed.
What was the error message?
/usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/Scrt1.o: In function
`_start':
(.text+0x20): undefined reference to `main'
collect2: error: ld returned 1 exit status
Makefile:3867: recipe for target 'libz3.so' failed
Might have something to do with -fPIE vs. -fPIC,
Right. Many build systems don't tolerate -fPIE/-pie out of the box. This
is explained in the dpkg-buildflags manpage, with hints how to fix it:
“Unconditionally passing -fPIE, -fpie or -pie to a build‐system using
libtool is safe as these flags will get stripped when building shared
libraries. Otherwise on projects that build both programs and shared
libraries you might need to make sure that when building the shared
libraries -fPIC is always passed last (so that it overrides any previous
-PIE) to compilation flags such as CFLAGS, and -shared is passed last
(so that it overrides any previous -pie) to linking flags such as
LDFLAGS.”
This is definitely not a regression, though,
That's right.
--
Jakub Wilk
Bug#830569: RFS: z3/4.4.1-0.1 [NMU] [4xRC]
Control: reopen -1 I have - added Breaks + Replaces in debian/control - fixed the copyright information for hamiltonian.py - enabled most tests - enabled hardening flags This should address the remaining issues the two of you found in the previous package. https://mentors.debian.net/package/z3 https://mentors.debian.net/debian/pool/main/z/z3/z3_4.4.1-0.1.dsc Regards, Fabian
Re: Bug#830569: RFS: z3/4.4.1-0.1 [NMU] [4xRC]
It looks like my last email was not forwarded to the debian-mentors
mailing list. Since I am still looking for a sponsor, here it is:
Hi Jakub,
thanks for the review!
On Sat, Jul 09, 2016 at 08:33:21PM +0200, Jakub Wilk wrote:
> Hi Fabian!
>
> I don't intend to sponsor this upload, but here's a quick review:
>
> * Fabian Wolff , 2016-07-09, 16:14:
> > * Add patch fix-dotnet-version.patch (Closes: #808695).
>
> This gives me no clue what the patch is about.
I have made the changelog entry a bit more verbose.
> > * Upgrade to Standards version 3.9.8 (no changes).
>
> I don't think this is a good idea for an NMU.
OK. Changed back to 3.9.6.
> > * Install shared libraries into new libz3-4 package (Closes: #819884).
>
> Now that the -dev package doesn't ship any ELFs, you should remove
> ${shlib:Depends} from -dev's Depends.
>
> "Pre-Depends: ${misc:Pre-Depends}" should be moved to the shared library
> package, or removed completely, because it's not needed these days.
I removed it, but does it do any harm?
> > * Install python files directly into /usr/lib/python2.7/dist-packages/
>
> AFAICS, upstream build system installs these files in the right place, so
> there should be no need to pick the *.py files from src/.
>
> These d/rules lines are effectively no-ops and should be removed:
>
> mkdir -p debian/tmp/usr/lib/python2.7/dist-packages/z3
> touch debian/tmp/usr/lib/python2.7/dist-packages/z3/__init__.py
>
> (The latter is probably a failed attempt of fixing #791604, which looks like
> a previous incarnation #819884.)
True, I fixed it. The first mkdir is necessary, though, to make the
directory debian/tmp/usr/lib/python2.7/dist-packages/. dh_auto_install
fails otherwise.
> > * Remove unnecessary version restriction of build dependency
> > cli-common-dev.
>
> Hmm, I don't know anything about CLI, but dh_cligacpolicy disagrees:
>
> dh_cligacpolicy: Warning! No Build-Depends(-Indep) on cli-common-dev (>=
> 0.5.7)!
#808405. Even oldoldstable ships 0.7.1, so it is safe to assume that
the version is >= 0.5.7.
> > * Format debian/control with cme.
>
> I don't think cosmetic changes are good idea for an NMU.
I undid them.
> > * Disable tests as they fail eventually.
>
> All the tests? :-O
It's more like one big one that calls individual functions that test
something. Most of the tests passed, but after about 1 GB (!) of test
output had been written on screen, something segfaulted. This is one
of those issues that probably need further investigation, but I lack
the overview over the test architecture to even just know where to
look. Here is the tail of the build log:
NUM_NON_LINEAR 0
NUM_ALIENS 0
NUM_THEORIES 0
END_PRIMITIVE_STATIC_FEATURES
(smt.preprocessing :time 0.01 :before-memory 5.25 :after-memory 5.25)
debian/rules:96: recipe for target 'override_dh_auto_test' failed
make[1]: *** [override_dh_auto_test] Segmentation fault
make[1]: Leaving directory '/build/z3-4.4.1'
debian/rules:9: recipe for target 'build' failed
make: *** [build] Error 2
dpkg-buildpackage: error: debian/rules build gave error exit status 2
This followed 987M of passing test logs, so I think this is not a
major issue.
> > I've tried building z3 with hardening flags turned on, but the build
> > failed.
>
> What was the error message?
/usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/Scrt1.o: In function
`_start':
(.text+0x20): undefined reference to `main'
collect2: error: ld returned 1 exit status
Makefile:3867: recipe for target 'libz3.so' failed
Might have something to do with -fPIE vs. -fPIC, but one would have to
investigate further to be sure. This is definitely not a regression,
though, since the z3 version currently in the archive has no hardening
flags enabled, either.
> > I don't know what the problem with the -dev package is; contrary to what
> > Lintian claims, it *does* contain a symlink to the respective shared
> > library.
>
> Yes, it does look like a bug in Lintian. Apparently it gets confused by the
> -ocaml-dev package:
>
> $ lintian libz3-4_4.4.1-0.1_amd64.deb libz3-dev_4.4.1-0.1_amd64.deb
> [nothing]
>
> $ lintian libz3-4_4.4.1-0.1_amd64.deb libz3-dev_4.4.1-0.1_amd64.deb
> libz3-ocaml-dev_4.4.1-0.1_amd64.deb
> W: libz3-4: dev-pkg-without-shlib-symlink usr/lib/x86_64-linux-gnu/libz3.so.4
> usr/lib/x86_64-linux-gnu/libz3.so
> W: libz3-ocaml-dev: hardening-no-relro usr/lib/ocaml/z3/dllz3ml.so
I have made the -dev package depend on libz3-4, and indeed, the
Lintian warning disappeared. Thanks for the hint!
The warning about the incompatible Java bytecode version might have
something to do with #829592, as I just noticed.
> > There are a few other issues that I was not able to fix, but I think
> > closing the four RC bugs has a higher priority right now.
>
> Absolutely. It's not NMUer obligation to fix every known bug.
>
> --
> Jakub Wilk
I have reuploaded the fixed version to Mentors
