Bug 555160 - Review Request: picosat - A SAT solver
Summary: Review Request: picosat - A SAT solver
Keywords:
Status: CLOSED ERRATA
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: David A. Wheeler
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks: 555161
TreeView+ depends on / blocked
 
Reported: 2010-01-13 20:37 UTC by Jerry James
Modified: 2010-01-21 00:14 UTC (History)
4 users (show)

Fixed In Version: 913-2.fc11
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2010-01-21 00:08:51 UTC
Type: ---
Embargoed:
dwheeler: fedora-review+
j: fedora-cvs+


Attachments (Terms of Use)

Description Jerry James 2010-01-13 20:37:49 UTC
Spec URL: http://jjames.fedorapeople.org/picosat/picosat.spec
SRPM URL: http://jjames.fedorapeople.org/picosat/picosat-913-1.fc12.src.rpm
Description:
PicoSAT solves the SAT problem, which is the classical NP-complete problem of searching for a satisfying assignment of a propositional formula in conjunctive normal form (CNF).  PicoSAT can generate proofs and cores in memory by compressing the proof trace.  It supports the proof format of TraceCheck.

Comment 1 Martin Gieseking 2010-01-17 19:37:24 UTC
Just some quick comments:

- you can drop gzip from Requires because it's picked up automatically

- the file permissions of the binaries should be changed to 755, e.g. by replacing cp with install:
  install -p -m 0755 libpicosat.so $RPM_BUILD_ROOT%{_libdir}/libpicosat.so.0.0.%{version}

  install -p -m 0755 picosat $RPM_BUILD_ROOT%{_bindir}


$ rpmlint /var/lib/mock/fedora-12-x86_64/result/picosat-*
picosat.x86_64: W: no-documentation
picosat.x86_64: E: non-standard-executable-perm /usr/bin/picosat 0775
picosat-devel.x86_64: W: no-documentation
picosat-libs.x86_64: E: non-standard-executable-perm /usr/lib64/libpicosat.so.0.0.913 0775
5 packages and 0 specfiles checked; 2 errors, 2 warnings.

Comment 2 David A. Wheeler 2010-01-17 23:57:57 UTC
Here's my review, using http://fedoraproject.org/wiki/Packaging:ReviewGuidelines
Basically:
 - Permisssions appear to wrong on some systems (per comment 1)
 - No docs; want to make some?
 - The license file is packaged into the "-libs" subpackage.  Shouldn't it be in the base package?
 - You don't *need* to "Requires: gzip"; go ahead and remove it.


    *  MUST: rpmlint must be run on every package. The output should be posted in the review.[1]

ISSUE: it appears there are permission issues on some systems per comment 1.  Also, no docs.

I built on a 32-bit Fedora 11 system:
  rpmlint picosat.spec ../RPMS/i586/picosat-* ../SRPMS/picosat-913-1.fc11.src.rpm 
It only gave this:
picosat.i586: W: no-documentation
picosat-devel.i586: W: no-documentation

Unlike comment 1, I didn't get an the rpmlint error on /usr/bin/picosat. Instead, I get the perfectly-fine -rwxr-xr-x for /usr/bin/picosat.  Still, if the permissions aren't right on some architectures, then perhaps it'd be best to use "install" as given in comment 1 to make sure that the permissions are correct everywhere. (Or use cp -p; chmod ... for the same effect).

There are no docs at all in the original package.  Yuk.

(Soapbox: What *is* this with SAT solver authors?  Are they just incapable of writing a short README or man page that explains the input and output format, command line parameters, and an example?!?  I appreciate that they've released the code, but some minimal documentation would help the non-mind-readers among us!)

Docs aren't required.  Still, having NO documentation is pretty sad.
I wrote a doc page for minisat2, which is available here:
   http://www.dwheeler.com/essays/minisat-user-guide.html
Maybe that could be used to create basic docs for picosat, pulling in its results from "picosat -h"?
Either an html file or a man page?

Docs aren't strictly *required*.
but *using* these tools without ANY documentation is, well, challenging.


    * MUST: The package must be named according to the Package Naming Guidelines.

OK.  It has several subpackages.  Many other Fedora packages for libraries use the "-libs" extension in the same, so it seems consistent.

    * MUST: The spec file name must match the base package %{name}, in the format %{name}.spec unless your package has an exemption. [2] .

OK

    * MUST: The package must meet the Packaging Guidelines

Looks fine.  For example, it patches the makefile so that $RPM_OPT_FLAGS apply.

    * MUST: The package must be licensed with a Fedora approved license and meet the Licensing Guidelines .

OK. (MIT)

    * MUST: The License field in the package spec file must match the actual license. [3]

OK.  Compared with:  http://www.opensource.org/licenses/mit-license.php

    * MUST: If (and only if) the source package includes the text of the license(s) in its own file, then that file, containing the text of the license(s) for the package must be included in %doc.[4]

POSSIBLE ISSUE.  The license file is packaged into the "-libs" subpackage.  Shouldn't it be in the base package?

    * MUST: The spec file must be written in American English. [5]

OK

    * MUST: The spec file for the package MUST be legible. [6]

OK

    * MUST: The sources used to build the package must match the upstream source, as provided in the spec URL. Reviewers should use md5sum for this task. If no upstream URL can be specified for this package, please see the Source URL Guidelines for how to deal with this.

OK.
wget http://fmv.jku.at/picosat/picosat-913.tar.gz
md5sum picosat-913.tar.gz /home/dwheeler/rpmbuild/SOURCES/picosat-913.tar.gz
e658fa16cd71ff2cafae190a905a93c6  picosat-913.tar.gz
e658fa16cd71ff2cafae190a905a93c6  /home/dwheeler/rpmbuild/SOURCES/picosat-913.tar.gz

    * MUST: The package MUST successfully compile and build into binary rpms on at least one primary architecture. [7]

OK.  Tested on 32-bit x86.

    * MUST: If the package does not successfully compile, build or work on an architecture, then those architectures should be listed in the spec in ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in bugzilla, describing the reason that the package does not compile/build/work on that architecture. The bug number MUST be placed in a comment, next to the corresponding ExcludeArch line. [8]

OK.
 koji build --scratch dist-f12 ./picosat-913-1.fc11.src.rpm 
 ...
 1928695 build (dist-f12, picosat-913-1.fc11.src.rpm): open (ppc09.phx2.fedoraproject.org) -> closed
   0 free  0 open  5 done  0 failed

    * MUST: All build dependencies must be listed in BuildRequires, except for any that are listed in the exceptions section of the Packaging Guidelines ; inclusion of those as BuildRequires is optional. Apply common sense.

OK.  The koji build (above) tested this.

    * MUST: The spec file MUST handle locales properly. This is done by using the %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.[9]

NA.  It doesn't have locales.

    * MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. [10]

OK.  Only the "-libs" subpackage stores shared libraries, and the spec file says:
 %post libs -p /sbin/ldconfig
 %postun libs -p /sbin/ldconfig
The "-devel" subpackage stores a .so file, but it's just a symlink.

    * MUST: Packages must NOT bundle copies of system libraries.[11]
OK

    * MUST: If the package is designed to be relocatable, the packager must state this fact in the request for review, along with the rationalization for relocation of that specific package. Without this, use of Prefix: /usr is considered a blocker. [12]

NA

    * MUST: A package must own all directories that it creates. If it does not create a directory that it uses, then it should require a package which does create that directory. [13]

OK.  It only creates a directory via %doc, which is handled by rpm.

    * MUST: A Fedora package must not list a file more than once in the spec file's %files listings. [14]

OK

    * MUST: Permissions on files must be set properly. Executables should be set with executable permissions, for example. Every %files section must include a %defattr(...) line. [15]

The permissions were fine in my test, however, see comment 1
for an issue on a 64-bit system.

    * MUST: Each package must have a %clean section, which contains rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [16]

OK

    * MUST: Each package must consistently use macros. [17]


OK.  It uses $RPM_BUILD_ROOT and ${RPM_OPT_FLAGS} style for these two, consistently.
(I suppose an argument could be made, because there are many %{...} uses,
but I think that it's fine.)


    * MUST: The package must contain code, or permissable content. [18]

OK.

    * MUST: Large documentation files must go in a -doc subpackage. (The definition of large is left up to the packager's best judgement, but is not restricted to size. Large can refer to either size or quantity). [19]

NA.  If only we had ANY documentation :-(.

    * MUST: If a package includes something as %doc, it must not affect the runtime of the application. To summarize: If it is in %doc, the program must run properly if it is not present. [19]

OK

    * MUST: Header files must be in a -devel package. [20]

OK

    * MUST: Static libraries must be in a -static package. [21]
NA

    * MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for directory ownership and usability). [22]
NA

    * MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1), then library files that end in .so (without suffix) must go in a -devel package. [20]
OK

    * MUST: In the vast majority of cases, devel packages must require the base package using a fully versioned dependency: Requires: %{name} = %{version}-%{release} [23]
OK

    * MUST: Packages must NOT contain any .la libtool archives, these must be removed in the spec if they are built.[21]
OK

    * MUST: Packages containing GUI applications must include a %{name}.desktop file, and that file must be properly installed with desktop-file-install in the %install section. If you feel that your packaged GUI application does not need a .desktop file, you must put a comment in the spec file with your explanation. [24]
NA

    * MUST: Packages must not own files or directories already owned by other packages. The rule of thumb here is that the first package to be installed should own the files or directories that other packages may rely upon. This means, for example, that no package in Fedora should ever share ownership with any of the files or directories owned by the filesystem or man package. If you feel that you have a good reason to own a file or directory that another package owns, then please present that at package review time. [25]
NA

    * MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [26]
OK

    * MUST: All filenames in rpm packages must be valid UTF-8. [27]
OK



FINALLY: Running it.

I installed & ran /usr/bin/picosat
and gave it this input:

c Here is a comment.
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

It parsed it, and correctly declared that it was satisfiable.

Comment 3 Jerry James 2010-01-18 19:05:16 UTC
I dropped the gzip Requires and rebuilt.  The automatic Requires generator did NOT pick it up.  I am building on an F-12 system.  Are either of you SURE that you saw gzip identified as a Requires by rpmbuild?

I don't know how the Requires generator could possibly find this anyway, since the dependency on gzip is hidden in C code (see app.c).

Regarding comment 1, Martin what is your default umask?  (Mine is 0022.)  I get the correct permissions when building on my machine, in mock, and with a koji scratch build.  David Wheeler also reports getting correct permissions in comment 2.  This makes me suspect that the problem is with your environment, rather than with the package.  In any case, koji-built packages will have correct permissions with the spec file as-is.  (Not that I object to using install instead of cp; I'll make that change anyway if I have to make a new package.)

The license file is in the correct place.  The -libs package is always installed, no matter what, but the so-called "base" package is optional.  Therefore, we need the license file where it will always be installed: the -libs package.

I considered adding http://fmv.jku.at/papers/Biere-JSAT08.pdf as documentation, but I'm not sure it would really help.  It talks about internal optimizations, rather than external interfaces.  I'm not competent to write documentation on the external interface anyway, since I don't understand it.  I only want this so I can get a functioning csisat, which I also don't understand, since I only want it to get a functioning blast. :-)

Comment 4 Martin Gieseking 2010-01-18 20:12:02 UTC
(In reply to comment #3)
> Regarding comment 1, Martin what is your default umask?  (Mine is 0022.)  I get
> the correct permissions when building on my machine, in mock, and with a koji
> scratch build.  David Wheeler also reports getting correct permissions in
> comment 2.  This makes me suspect that the problem is with your environment,
> rather than with the package.

Your guess was right. The umask on my notebook was set to 0002. After modifying it, the rpmlint errors went away. Sorry for the noise. :)

Comment 5 David A. Wheeler 2010-01-18 23:34:54 UTC
> The automatic Requires generator did NOT pick [up gzip].

Okay.  Could you please insert a comment above the Requires: documenting that the gzip is not automatically picked up by rpm, e.g., something like:
# gzip required; rpm can't determine this because it is hidden in C code app.c.

As noted in comment 4, the permissions are fine, so no change to the package is needed for permissions.

Could you please add a comment to the spec file explaining why the *base* package has no license file?  Anyone running rpmlint on this package will notice this issue, so let's head off that problem now.  Something like this:
# The license file is placed in the "-libs" package, not the base package,
# because the "-libs" package is always installed when any of these packages
# are installed, but it's possible to install -libs without the base.

> I considered adding http://fmv.jku.at/papers/Biere-JSAT08.pdf as documentation,
but I'm not sure it would really help.  It talks about internal optimizations,
rather than external interfaces.

Never mind the internal documentation.  I agree with you, that won't help.

Here's an alternative.  I wrote up a short man page, based on "picosat -h" and the documentation I wrote for minisat2.  Would you please add it to the package (installed as with any man page), and submit it to upstream for them to consider adding in a future version?  It doesn't solve the universe's problems, but it's hard to use programs with ZERO documentation:
http://www.dwheeler.com/essays/picosat.1

(Technically documentation is only a SHOULD, but it's an important SHOULD, and I'd rather there be SOMETHING useful.)

Comment 6 Jerry James 2010-01-19 17:03:40 UTC
I made the changes requested in comment 5.  New URLs:

Spec URL: http://jjames.fedorapeople.org/picosat/picosat.spec
SRPM URL: http://jjames.fedorapeople.org/picosat/picosat-913-2.fc12.src.rpm

Thanks for the man page!

Comment 7 David A. Wheeler 2010-01-19 17:48:23 UTC
I rebuilt release 2 on a Fedora 12, x86_64 box.  Everything looks great!  Here are the details.

rpmlint results were fine:
rpmlint picosat.spec ../RPMS/x86_64/picosat-*-2* ../SRPMS/picosat-913-2.fc12.src.rpm 
picosat-devel.x86_64: W: no-documentation
5 packages and 1 specfiles checked; 0 errors, 1 warnings.
(The docs are in another subpackage, not -devel; that's fine.)

The issues in comment 5 were addressed (mainly commenting to explain why certain things were done.)

I did an rpmls on all binary rpms; the permissions are fine.

I installed it. "man picosat" did what you'd expect.
I ran "picosat" with this input:
c Here is a comment.
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

And again, it correctly declared that it was "satisfiable".

Packaging
APPROVED.

Comment 8 Jerry James 2010-01-19 19:21:51 UTC
Thanks, David!

New Package CVS Request
=======================
Package Name: picosat
Short Description: A SAT solver
Owners: jjames
Branches: F-11 F-12
InitialCC:

Comment 9 Jason Tibbitts 2010-01-19 19:23:59 UTC
CVS done (by process-cvs-requests.py).

Comment 10 Fedora Update System 2010-01-19 21:07:37 UTC
picosat-913-2.fc12 has been submitted as an update for Fedora 12.
http://admin.fedoraproject.org/updates/picosat-913-2.fc12

Comment 11 Fedora Update System 2010-01-19 21:07:41 UTC
picosat-913-2.fc11 has been submitted as an update for Fedora 11.
http://admin.fedoraproject.org/updates/picosat-913-2.fc11

Comment 12 Fedora Update System 2010-01-21 00:08:46 UTC
picosat-913-2.fc12 has been pushed to the Fedora 12 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 13 Fedora Update System 2010-01-21 00:14:18 UTC
picosat-913-2.fc11 has been pushed to the Fedora 11 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.