Bug 428410 - Review Request: LADR - Library for Automated Deduction Research
Review Request: LADR - Library for Automated Deduction Research
Status: CLOSED DUPLICATE of bug 451996
Product: Fedora
Classification: Fedora
Component: Package Review (Show other bugs)
All Linux
low Severity medium
: ---
: ---
Assigned To: Nobody's working on this, feel free to take it
Fedora Extras Quality Assurance
Depends On:
  Show dependency treegraph
Reported: 2008-01-11 05:30 EST by Tim Colles
Modified: 2009-05-22 12:55 EDT (History)
4 users (show)

See Also:
Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of:
Last Closed: 2008-06-29 12:40:30 EDT
Type: ---
Regression: ---
Mount Type: ---
Documentation: ---
Verified Versions:
Category: ---
oVirt Team: ---
RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: ---

Attachments (Terms of Use)

  None (edit)
Description Tim Colles 2008-01-11 05:30:36 EST
Spec URL: http://homepages.inf.ed.ac.uk/timc/repos/fedora8/SPECS/LADR.spec
SRPM URL: http://homepages.inf.ed.ac.uk/timc/repos/fedora8/SRPMS/LADR-200712-1.src.rpm
Description: Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the
successor of the Otter prover.
Comment 1 Tim Colles 2008-01-11 05:49:28 EST
This is my first package, and you am seeking a sponsor.
Comment 2 Alec Leamas 2008-01-11 09:05:38 EST
This is just an informal review, you still need a sponsor. But here it is:

Naming: Since you are the upstream maintainer, I guess you are free to use LADR
instead of ladr. However, if there are no particular reasons to use capital
letters, uing lowercase would fit better into the Fedora naming scheme.

Licensing: GPL file included, GPL preamnble in all C files. No overall GPLL
statement for the complete package, no GPL header inn python scripts. Don't know
what to think about this, I'm a rookie.

testing. This package install ~35 files into /usr/bin. The docs are somewhat
hard to find - the reference to the manual in README.first is wrong, and the
programs don't understand standard '-h'/'..help' options. It's possible to
invoke some tools without segfaulting.  The website URL is fine. Once again,
don't know what to think

OK Rpmlint is silent
OK Spec file name.
OK Licensing.
OK License: field matches sw.
OK License included in doc.
OK Spec file in American English: I'm from Sweden, but to ny understanding...
OK Spec file legible
OK Source MD5sum: 6e2896ed4cce4556bfcc321778df5dfe upstream and in src.rpm
OK Builds on i386
OK See no reason to exclude architecture(s)
OK All build dependencies listed  (mock test OK)
OK Locales management - this package is not localized.
OK Libraries (no libraries in this package)
OK Not relocateble.
OK Owns it's directories.
OK No %file duplicates
OK File permissions
OK %clean target
OK Consistent macro usage
OK Code/permissive content (this is just code).
OK No large documentation
OK Doc's don't affect runtime.
OK No header files
OK No static libraries
OK No pkgconfig file(s)
OK No libraries
OK No devel package
OK Not a GUI application
OK Does not own other package's file/dirs.
OK rm -rf %{buildroot} in %install
OK Valid filenames (just ASCII)
OK No scriplets
OK No subpackages
OK No pkgconfig files
OK No file dependencies

Comment 3 Tim Colles 2008-01-11 10:08:47 EST
Thanks for your comments. I am not the upstream maintainer and the name LADR is
an acronym so keeping the uppercase seemed more appropriate - no problem to
change it if that is the preferred option.

Not sure about the GPL stuff - could I just apply a patch to add the missing GPL
statements and then inform upstream to add them?

Regarding "The docs are somewhat hard to find - the reference to the manual in
README.first is wrong, and the programs don't understand standard '-h'/'..help'
options." - I am not sure to what extent I should be modifying an upstream
package (and the code in the case of adding help options) in order to get a
package accepted as the guidelines make no mention of this - were I the actual
maintainer of the package I could see that this would be good of course.
Comment 4 Alec Leamas 2008-01-11 12:59:47 EST
Well, I'm a rookie as you, but as see it:

- The Packaging/NamingGuidelines has a separate header "Case Sensitivity".
  I suggest you read it and interpret the upstream requirements in
  that context. 
- To my understanding, this situation is covered by Licensing/FAQ, the 
  first entry. Basically, this boils down to "contact upstream".
- Things like the bad filename could be fixed by a  patch (preferably
  taking the installations directory /usr/share/LADR into account). The 
  rest of the comments are, as you have noticed, aimed for the upstream
  maintainer. And this is not you... sorry I got it wrong.

Sorry (embarrassed!) for all typos. I lost what I had written, and had to
rewrite it being all but happy :-)
Comment 5 Mamoru TASAKA 2008-01-27 11:36:08 EST
Well, first of all there are some files under %_bindir of which names
are too generic and may cause name space conflict like:

attack or looper or renamer or so.

Isn't it possible to have binaries under %_bindir have some prefix name
related to LADR, or move binaries under %_bindir to some directory like
Comment 6 Tim Colles 2008-01-31 10:10:44 EST
Sent a patch to upstream to add GPL statements to Python scripts and fix the
readme manual link. They intend to include this patch in the next release
(hopefully February).

Not sure I understand the requirement, eg. there can be no %_bindir/attack
because something at some point might need to be called %_bindir/attack? This is
however a specialized package so I could certainly ask upstream if they can be
renamed, or easier probably to just rename them ladr_* for the purposes of
putting this on Fedora.
Comment 7 Mamoru TASAKA 2008-01-31 11:43:04 EST
Well, the names like "renamer" or "attack" are too generic and
such naming should be avoided for binaries under %_bindir.

Renaming to ladr_XXX or so is one of the possible solutions.
Comment 8 David A. Wheeler 2008-05-29 01:39:08 EDT
I strongly suggest that this be renamed to "prover9" or "prover9-mace4".

LADR is just the low-level shared library used to implement prover9 and mace4.
Users don't normally see LADR directly; they'll typically just use
prover9 and mace4.  Even the description gives this away - it talks about the
user-visible programs prover9 and mace4, and not the lower-level library for them.
MANY programs have tools to access lower-level data structures, but typically
the package is named after the upper-level, user-visible component.

For a point of reference, Debian names the same package "prover9".

Having prover9/mace4 packaged for Fedora is of HIGH importance to me.
Comment 9 Tim Colles 2008-05-30 08:14:11 EDT
Good plan. I am going to resubmit this next week as "prover9" to FC9 with a
local patch (as far as I know the upstream developer has not produced a new
release including this patch), hopefully then someone will sponsor it going into
the Extras repository.
Comment 10 Mamoru TASAKA 2008-06-29 12:40:30 EDT

*** This bug has been marked as a duplicate of 451996 ***

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