[Bug 812681] Review Request: GlueMiniSat - Boolean SAT solver that implements literal blocks distance (LBD)

bugzilla at redhat.com bugzilla at redhat.com
Tue Apr 24 18:20:24 UTC 2012


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=812681

--- Comment #3 from John C Peterson <jcp at eskimo.com> 2012-04-24 14:20:22 EDT ---

Spec URL: http://www.eskimo.com/~jcp/glueminisat.spec
SRPM URL: http://www.eskimo.com/~jcp/glueminisat-2.2.5-2.fc16.src.rpm

I think I have taken care of most of the loose ends in this version. I sent
both of the patches to the upstream author Nabeshima Hidetomo and received a
prompt reply. He said he would be applying the patches to his next release, and
pointed out another small tweak to the printf patch to keep the console output
from line wrapping.

No argument here on the less than complete documentation. I was going to
suggest writing up a small HTML page for %doc with a short overview, links to
the GlueMiniSat home page, and to David Wheeler's online tutorial for vanilla
MiniSat with a few words about the extra command line options, namely -glucose
and -minisat. Any thoughts on a better format or approach?

I double checked the words that rpmlint claims are mispelled and they all check
out (many dictionaries seem to be lacking in knowledge of technically oriented
words, no stranger to that problem).

John


% rpmlint -v glueminisat.spec ../SRPMS/glueminisat-2.2.5-2.fc16.src.rpm
../RPMS/x86_64/glueminisat-2.2.5-2.fc16.x86_64.rpm
glueminisat.spec: I: checking-url
https://sites.google.com/a/nabelab.org/glueminisat/home/download/glueminisat-2.2.5.tar.gz
(timeout 10 seconds)
glueminisat.src: I: checking
glueminisat.src: W: spelling-error %description -l en_US boolean -> Boolean,
boo lean, boo-lean
glueminisat.src: W: spelling-error %description -l en_US satisfiability ->
insatiability, advisability
glueminisat.src: W: spelling-error %description -l en_US learnt -> learn,
learns, learn t
glueminisat.src: W: spelling-error %description -l en_US nd -> ND, Nd, n
glueminisat.src: W: spelling-error %description -l en_US unsatisfiable ->
unsatisfied, unjustifiable
glueminisat.src: W: spelling-error %description -l en_US minisat -> mini sat,
mini-sat, minis at
glueminisat.src: I: checking-url http://glueminisat.nabelab.org/ (timeout 10
seconds)
glueminisat.src: I: checking-url
https://sites.google.com/a/nabelab.org/glueminisat/home/download/glueminisat-2.2.5.tar.gz
(timeout 10 seconds)
glueminisat.x86_64: I: checking
glueminisat.x86_64: W: spelling-error %description -l en_US boolean -> Boolean,
boo lean, boo-lean
glueminisat.x86_64: W: spelling-error %description -l en_US satisfiability ->
insatiability, advisability
glueminisat.x86_64: W: spelling-error %description -l en_US learnt -> learn,
learns, learn t
glueminisat.x86_64: W: spelling-error %description -l en_US nd -> ND, Nd, n
glueminisat.x86_64: W: spelling-error %description -l en_US unsatisfiable ->
unsatisfied, unjustifiable
glueminisat.x86_64: W: spelling-error %description -l en_US minisat -> mini
sat, mini-sat, minis at
glueminisat.x86_64: I: checking-url http://glueminisat.nabelab.org/ (timeout 10
seconds)
glueminisat.x86_64: W: no-manual-page-for-binary glueminisat
2 packages and 1 specfiles checked; 0 errors, 13 warnings.

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.



More information about the package-review mailing list