Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
Summary: Review Request: gappa - Prove programs with floating-point or fixed-point arithmetic
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Summary: Review Request: gappa - Prove programs with floating-point or fixed-point arithmetic Product: Fedora Version: rawhide Platform: All OS/Version: Linux Status: NEW Severity: medium Priority: medium Component: Package Review AssignedTo: nobody@fedoraproject.org ReportedBy: dwheeler@dwheeler.com QAContact: extras-qa@fedoraproject.org CC: notting@redhat.com, fedora-package-review@redhat.com Estimated Hours: 0.0 Classification: Fedora
Spec URL: http://www.dwheeler.com/SPECS/gappa.spec SRPM URL: http://www.dwheeler.com/SRPMS/gappa-0.13.0-1.fc13.src.rpm Description: Gappa is a tool intended to help verifying and formally prove properties on numerical programs and circuits handling floating-point or fixed-point arithmetic. This tool manipulates logical formulas stating the enclosures of expressions in some intervals. Through the use of rounding operators as part of the expressions, Gappa is specially designed to deal with formulas that could appear when certifying numerical codes. In particular, Gappa makes it simple to bound computational errors due to floating-point arithmetic. The tool and its documentation were written by Guillaume Melquiond.
Running rpmlint only produces one warning (because there is no manual upstream): rpmlint ./gappa.spec ../RPMS/i686/gappa-0.13.0-1.fc13.i686.rpm ../SRPMS/gappa-0.13.0-1.fc13.src.rpm gappa.i686: W: no-manual-page-for-binary gappa 2 packages and 1 specfiles checked; 0 errors, 1 warnings.
Koji builds are fine on F13 and F14: koji build --scratch dist-f14 ~/rpmbuild/SRPMS/gappa-0.13.0-1.fc13.src.rpm ... Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=2387684 ... 0 free 0 open 3 done 0 failed 2387684 build (dist-f14, gappa-0.13.0-1.fc13.src.rpm) completed successfully
koji build --scratch dist-f13 ~/rpmbuild/SRPMS/gappa-0.13.0-1.fc13.src.rpm ... Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=2387687 ... 0 free 0 open 3 done 0 failed 2387687 build (dist-f13, gappa-0.13.0-1.fc13.src.rpm) completed successfully
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Mark Rader msrader@gmail.com changed:
What |Removed |Added ---------------------------------------------------------------------------- CC| |msrader@gmail.com AssignedTo|nobody@fedoraproject.org |msrader@gmail.com
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Jussi Lehtola jussi.lehtola@iki.fi changed:
What |Removed |Added ---------------------------------------------------------------------------- CC| |jussi.lehtola@iki.fi
--- Comment #1 from Jussi Lehtola jussi.lehtola@iki.fi 2010-08-09 18:09:31 EDT --- URL should be http://gappa.gforge.inria.fr/ .
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Martin Gieseking martin.gieseking@uos.de changed:
What |Removed |Added ---------------------------------------------------------------------------- CC| |martin.gieseking@uos.de
--- Comment #2 from Martin Gieseking martin.gieseking@uos.de 2010-09-10 13:58:46 EDT --- Here are some more notes:
- you can drop the two variable definitions from %configure
- preserve the timestamp of file COPYING http://fedoraproject.org/wiki/Packaging_tricks#Convert_encoding_to_UTF-8
- use macros (%{_bindir}, %{_defaultdocdir}) in %install and %files
- instead of running your own test, I recommend to run the bundled testsuite (with "make check"). However, in order to ensure that rpmbuild fails on a test failure, the Makefile must be slightly adapted. Here's a quick sed hack, but patching testsuite/Makefile.am accordingly would be much better: sed -i 's/( cat "$$logtmp"; \)/\1\n\texit 1; \/' testsuite/Makefile
Maybe upstream can add the "exit 1" (or something similar) to the sources.
- I suggest to replace the directory %{_defaultdocdir}/doc with the pdf manual available from the upstream website http://gappa.gforge.inria.fr/gappa.pdf as the currently installed folders don't contain a usable manual but the sources required to build the manual. You can also try to build the pdf file from these sources (requires dblatex and some additional tools).
- drop INSTALL from the docs
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #3 from David A. Wheeler dwheeler@dwheeler.com 2010-09-10 17:43:12 EDT --- Okay, I have addressed all the issues noted in comment 1 and comment 2.
The updated package is here: Spec URL: http://www.dwheeler.com/SPECS/gappa.spec SRPM URL: http://www.dwheeler.com/SRPMS/gappa-0.13.0-2.fc13.src.rpm
I changed the URL per comment 1.
Regarding comment 2: - you can drop the two variable definitions from %configure
DONE
- preserve the timestamp of file COPYING http://fedoraproject.org/wiki/Packaging_tricks#Convert_encoding_to_UTF-8
DONE
- use macros (%{_bindir}, %{_defaultdocdir}) in %install and %files
DONE. I also globally defined another macro to clean it up.
- instead of running your own test, I recommend to run the bundled testsuite (with "make check"). However, in order to ensure that rpmbuild fails on a test failure, the Makefile must be slightly adapted. Here's a quick sed hack, but patching testsuite/Makefile.am accordingly would be much better: sed -i 's/( cat "$$logtmp"; \)/\1\n\texit 1; \/' testsuite/Makefile Maybe upstream can add the "exit 1" (or something similar) to the sources.
DONE.
I kept my own test and ADDED the bundled testsuite; the more the merrier.
Instead of futzing with Makefile.am directly, I'm using the sed mod, and have sent an email to the author asking that the upstream makefile be changed. In the long term it'd be best if *upstream* made the change.
- I suggest to replace the directory %{_defaultdocdir}/doc with the pdf manual available from the upstream website http://gappa.gforge.inria.fr/gappa.pdf as the currently installed folders don't contain a usable manual but the sources required to build the manual. You can also try to build the pdf file from these sources (requires dblatex and some additional tools).
DONE.
I can't build the PDF easily; it requires tools that aren't packaged. If someone wants to package THOSE tools up, great.
- drop INSTALL from the docs
DONE.
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #4 from David A. Wheeler dwheeler@dwheeler.com 2010-09-11 12:23:45 EDT --- I've made some additional changes to the package, it's now here: Spec URL: http://www.dwheeler.com/SPECS/gappa.spec SRPM URL: http://www.dwheeler.com/SRPMS/gappa-0.13.0-3.fc13.src.rpm
After I posted the previous version, I realized that I *had* added the PDF, but had *not* removed the doc sources. I once I did that, I found I could simplify the package spec further, which is a good thing.
rpmlint results for this release 3 have no errors, and although it has no man page, it DOES have pdf documentation: rpmlint gappa.spec ../SRPMS/gappa-0.13.0-3.fc13.src.rpm ../RPMS/x86_64/gappa-0.13.0-3.fc13.x86_64.rpm ../RPMS/x86_64/gappa-debuginfo-0.13.0-3.fc13.x86_64.rpm gappa.x86_64: W: no-manual-page-for-binary gappa 3 packages and 1 specfiles checked; 0 errors, 1 warnings.
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #5 from Martin Gieseking martin.gieseking@uos.de 2010-09-12 05:48:59 EDT --- Mark, are you going to do the review of this package? Otherwise, I would take it.
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Martin Gieseking martin.gieseking@uos.de changed:
What |Removed |Added ---------------------------------------------------------------------------- Status|NEW |ASSIGNED AssignedTo|msrader@gmail.com |martin.gieseking@uos.de Flag| |fedora-review+
--- Comment #6 from Martin Gieseking martin.gieseking@uos.de 2010-09-16 13:44:59 EDT --- Since Mark didn't respond, I do the formal review.
David, the package looks fine and is ready now. However, please remove the comment above the %files section (about the %doc macro) as it isn't valid any longer. ;-)
Also, the copyright notice in the source files looks a bit strange because of the missing GPL version number: "... under the terms of the GNU General Public License version." Maybe you can ask upstream to fix it in a future release by adding the intended version number.
$ rpmlint /var/lib/mock/fedora-13-x86_64/result/*.rpm gappa.x86_64: W: no-manual-page-for-binary gappa 3 packages and 0 specfiles checked; 0 errors, 1 warnings.
The warning is expected and can be ignored.
--------------------------------- key:
[+] OK [.] OK, not applicable [X] needs work ---------------------------------
[+] MUST: The package must be named according to the Package Naming Guidelines. [+] MUST: The spec file name must match the base package %{name}. [+] MUST: The package must meet the Packaging Guidelines. [+] MUST: The package must be licensed with a Fedora approved license. - GPLv2 or CeCILL accirding to file README and COPYING.GPL
[+] MUST: The License field in the package spec file must match the actual license. [+] MUST: The file containing the text of the license(s) must be included in %doc. [+] MUST: The spec file must be written in American English. [+] MUST: The spec file for the package MUST be legible. [+] MUST: The sources used to build the package must match the upstream source. $ md5sum gappa-0.13.0.tar.gz* 27a09741f6b4da4c46c85952102af651 gappa-0.13.0.tar.gz 27a09741f6b4da4c46c85952102af651 gappa-0.13.0.tar.gz.1
$ md5sum gappa.pdf* 15be2bc2e5fc88ff5addea92b85c44ea gappa.pdf 15be2bc2e5fc88ff5addea92b85c44ea gappa.pdf.1
[+] MUST: The package MUST successfully compile and build into binary rpms on at least one primary architecture. Koji scratch build: http://koji.fedoraproject.org/koji/taskinfo?taskID=2471643
[.] MUST: If the package does not successfully compile, ... [+] MUST: All build dependencies must be listed in BuildRequires. [.] MUST: The spec file MUST handle locales properly. [.] MUST: Packages storing shared library files must call ldconfig in %post and %postun. [+] MUST: Packages must NOT bundle copies of system libraries. [.] MUST: If the package is designed to be relocatable, ... [+] MUST: A package must own all directories that it creates. [+] MUST: A Fedora package must not list a file more than once in %files. [+] MUST: Permissions on files must be set properly. [+] MUST: Each package must consistently use macros. [+] MUST: The package must contain code, or permissable content. [.] MUST: Large documentation files must go in a -doc subpackage. [+] MUST: Files in %doc must not affect the runtime of the application. [.] MUST: Header files must be in a -devel package. [.] MUST: Static libraries must be in a -static package. [.] MUST: .so files (without suffix) must go in a -devel package. [.] MUST: devel packages must require the base package. [+] MUST: Packages must NOT contain any .la libtool archives. [.] MUST: Packages containing GUI applications must include a %{name}.desktop file. [+] MUST: Packages must not own files or directories already owned by other packages. [+] MUST: All filenames in rpm packages must be valid UTF-8.
[.] SHOULD: If the source package does not include license text(s) ... [+] SHOULD: The reviewer should test that the package builds in mock. [+] SHOULD: The package should compile and build into binary rpms on all supported architectures. [+] SHOULD: The reviewer should test that the package functions as described. [.] SHOULD: If scriptlets are used, those scriptlets must be sane. [.] SHOULD: Subpackages other than devel should require the base package. [.] SHOULD: pkgconfig(.pc) files should be placed in a -devel pkg. [.] SHOULD: If the package has file dependencies outside of /etc, /bin, /sbin, /usr/bin, or /usr/sbin ... [X] SHOULD: your package should contain man pages for binaries/scripts. - A manpage would be nice, but that's optional of course.
---------------- Package APPROVED ----------------
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #7 from Mark Rader msrader@gmail.com 2010-09-16 14:07:53 EDT --- MArtin
Thanks, I apologize for my tardiness. I am quite happy to have you review this.
Mark
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #8 from Martin Gieseking martin.gieseking@uos.de 2010-09-16 14:22:58 EDT --- (In reply to comment #7)
Thanks, I apologize for my tardiness. I am quite happy to have you review this.
Mark, thanks for the feedback. I hope you wasn't about to do the review. Next time I'll wait some days longer before I hijack a Bugzilla ticket. :)
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #9 from David A. Wheeler dwheeler@dwheeler.com 2010-09-18 19:35:35 EDT --- Martin Gieseking *AND* Mark Rader - thanks very much!! I can think of worse problems than people fighting to review my package :-).
I agree that a manpage would be nice, but as noted, it's optional. Since the package includes .pdf documentation, I don't think it's so critical; at least there is SOME documentation. I'll remove the extraneous comment when I submit it.
THANKS.
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #10 from David A. Wheeler dwheeler@dwheeler.com 2010-09-18 19:44:45 EDT --- New Package SCM Request ======================= Package Name: gappa Short Description: Prove programs with floating-point or fixed-point arithmetic Owners: dwheeler mrader amdunn jjames Branches: f13 f14 InitialCC: dwheeler
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
David A. Wheeler dwheeler@dwheeler.com changed:
What |Removed |Added ---------------------------------------------------------------------------- Flag| |fedora-cvs?
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #11 from Kevin Fenzi kevin@tummy.com 2010-09-19 15:24:41 EDT --- Git done (by process-git-requests).
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Fedora Update System updates@fedoraproject.org changed:
What |Removed |Added ---------------------------------------------------------------------------- Status|ASSIGNED |MODIFIED
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #12 from Fedora Update System updates@fedoraproject.org 2010-09-25 23:54:53 EDT --- gappa-0.13.0-4.fc14 has been submitted as an update for Fedora 14. https://admin.fedoraproject.org/updates/gappa-0.13.0-4.fc14
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #13 from Fedora Update System updates@fedoraproject.org 2010-09-25 23:55:01 EDT --- gappa-0.13.0-4.fc13 has been submitted as an update for Fedora 13. https://admin.fedoraproject.org/updates/gappa-0.13.0-4.fc13
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Fedora Update System updates@fedoraproject.org changed:
What |Removed |Added ---------------------------------------------------------------------------- Status|MODIFIED |ON_QA
--- Comment #14 from Fedora Update System updates@fedoraproject.org 2010-09-26 23:37:42 EDT --- gappa-0.13.0-4.fc14 has been pushed to the Fedora 14 testing repository. If problems still persist, please make note of it in this bug report. If you want to test the update, you can install it with su -c 'yum --enablerepo=updates-testing update gappa'. You can provide feedback for this update here: https://admin.fedoraproject.org/updates/gappa-0.13.0-4.fc14
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #15 from Fedora Update System updates@fedoraproject.org 2010-10-05 09:19:50 EDT --- gappa-0.13.0-4.fc14 has been pushed to the Fedora 14 stable repository. If problems still persist, please make note of it in this bug report.
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Fedora Update System updates@fedoraproject.org changed:
What |Removed |Added ---------------------------------------------------------------------------- Status|ON_QA |CLOSED Fixed In Version| |gappa-0.13.0-4.fc14 Resolution| |ERRATA Last Closed| |2010-10-05 09:19:55
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
--- Comment #16 from Fedora Update System updates@fedoraproject.org 2010-10-08 16:36:41 EDT --- gappa-0.13.0-4.fc13 has been pushed to the Fedora 13 stable repository. If problems still persist, please make note of it in this bug report.
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug.
https://bugzilla.redhat.com/show_bug.cgi?id=622173
Fedora Update System updates@fedoraproject.org changed:
What |Removed |Added ---------------------------------------------------------------------------- Fixed In Version|gappa-0.13.0-4.fc14 |gappa-0.13.0-4.fc13
package-review@lists.fedoraproject.org