Bug 622173 - Review Request: gappa - Prove programs with floating-point or fixed-point arithmetic
Summary: Review Request: gappa - Prove programs with floating-point or fixed-point ari...
Keywords:
Status: CLOSED ERRATA
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Martin Gieseking
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2010-08-07 22:06 UTC by David A. Wheeler
Modified: 2010-10-08 20:36 UTC (History)
5 users (show)

Fixed In Version: gappa-0.13.0-4.fc13
Clone Of:
Environment:
Last Closed: 2010-10-05 13:19:55 UTC
Type: ---
Embargoed:
martin.gieseking: fedora-review+
kevin: fedora-cvs+


Attachments (Terms of Use)

Description David A. Wheeler 2010-08-07 22:06:21 UTC
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

Comment 1 Susi Lehtola 2010-08-09 22:09:31 UTC
URL should be http://gappa.gforge.inria.fr/ .

Comment 2 Martin Gieseking 2010-09-10 17:58:46 UTC
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

Comment 3 David A. Wheeler 2010-09-10 21:43:12 UTC
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.

Comment 4 David A. Wheeler 2010-09-11 16:23:45 UTC
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.

Comment 5 Martin Gieseking 2010-09-12 09:48:59 UTC
Mark, are you going to do the review of this package? Otherwise, I would take it.

Comment 6 Martin Gieseking 2010-09-16 17:44:59 UTC
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
----------------

Comment 7 Mark Rader 2010-09-16 18:07:53 UTC
MArtin

Thanks, I apologize for my tardiness.  I am quite happy to have you review this.

Mark

Comment 8 Martin Gieseking 2010-09-16 18:22:58 UTC
(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. :)

Comment 9 David A. Wheeler 2010-09-18 23:35:35 UTC
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.

Comment 10 David A. Wheeler 2010-09-18 23:44:45 UTC
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

Comment 11 Kevin Fenzi 2010-09-19 19:24:41 UTC
Git done (by process-git-requests).

Comment 12 Fedora Update System 2010-09-26 03:54:53 UTC
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

Comment 13 Fedora Update System 2010-09-26 03:55:01 UTC
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

Comment 14 Fedora Update System 2010-09-27 03:37:42 UTC
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

Comment 15 Fedora Update System 2010-10-05 13:19:50 UTC
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.

Comment 16 Fedora Update System 2010-10-08 20:36:41 UTC
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.


Note You need to log in before you can comment on or make changes to this bug.