Bug 451996 - Review Request: prover9 - Thereom Prover and Countermodel Generator
Review Request: prover9 - Thereom Prover and Countermodel Generator
Product: Fedora
Classification: Fedora
Component: Package Review (Show other bugs)
All Linux
low Severity medium
: ---
: ---
Assigned To: Mamoru TASAKA
Fedora Extras Quality Assurance
: 428410 (view as bug list)
Depends On:
  Show dependency treegraph
Reported: 2008-06-18 11:29 EDT by Tim Colles
Modified: 2008-08-07 19:51 EDT (History)
4 users (show)

See Also:
Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of:
Last Closed: 2008-08-06 06:18:57 EDT
Type: ---
Regression: ---
Mount Type: ---
Documentation: ---
Verified Versions:
Category: ---
oVirt Team: ---
RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: ---
mtasaka: fedora‑review+
kevin: fedora‑cvs+

Attachments (Terms of Use)

  None (edit)
Description Tim Colles 2008-06-18 11:29:21 EDT
Spec URL: http://homepages.inf.ed.ac.uk/timc/prover9/prover9.spec
SRPM URL: http://homepages.inf.ed.ac.uk/timc/prover9/prover9-200805a-1.src.rpm

I am seeking a sponsor!

This is a port of the Debian equivalent package. This version supercedes an
earlier version that was submitted for review named LADR (#428410)


This package provides the Prover9 resolution/paramodulation theorem prover
and the Mace4 countermodel generator.

Prover9 is an automated theorem prover for first-order and equational logic.
It is a successor of the Otter prover. Prover9 uses the inference techniques
of ordered resolution and paramodulation with literal selection.

The program Mace4 searches for finite structures satisfying first-order and
equational statements, the same kind of statement that Prover9 accepts. If
the statement is the denial of some conjecture, any structures found by
Mace4 are counterexamples to the conjecture.

Mace4 can be a valuable complement to Prover9, looking for counterexamples
before (or at the same time as) using Prover9 to search for a proof. It can
also be used to help debug input clauses and formulas for Prover9.
Comment 1 Mamoru TASAKA 2008-06-29 12:40:31 EDT
*** Bug 428410 has been marked as a duplicate of this bug. ***
Comment 2 Mamoru TASAKA 2008-06-29 14:01:45 EDT
Some random comments on 200805a-1:

* About prover9-libtoolise.patch
  - This patch seems to be for providing shared library named libladr.so.4.
    However if the original tarball does not provide any shared library
    by default, this way is dangerous because we cannot guess with what
    soversion the upstream developer comes to provide shared library in
    the future. At this stage the number "4:0:0" can be chosen arbitrarily
    without any ground.
    See also the explanation by Patrice Dumas:

    So if this package only provides static archives by default, please
    of "static libraries only".

* Compilation flags
  - This package completely ignores Fedora specific compilation flags:
    You can check what flags must be passed by
    $ rpm --eval %optflags

    This also reads to creating non-useful debuginfo rpm.

* Timestamps
  - When using %__install or %__cp commands, add "-p" option to keep timestamps
    on installed files.

* Unneeded ldconfig call
  - This -devel package does not need to call /sbin/ldconfig on scriptlets.

* Too generic names
  - Again filenames like "attack" or "renamer", "rewriter", etc... are
    too generic for files to be installed under %_bindir.
    Also it may be that the names "isofilter?" are also dangerous, as
    my system already has "iso-info" or "isoinfo" (!!!!) or "isosize" or
    so. Would you rename these binaries to "prover9-???" or move these
    under %_libdir/%name , for example?
Comment 3 Tim Colles 2008-07-04 06:04:36 EDT
Thanks for looking at this Mamoru. The new release at:

  Spec URL: http://homepages.inf.ed.ac.uk/timc/prover9/prover9.spec
  SRPM URL: http://homepages.inf.ed.ac.uk/timc/prover9/prover9-200805a-2.src.rpm

fixes all these:

  * About prover9-libtoolise.patch
    This patch has been dropped and the static library added to -devel (which
    also provides a virtual -static).

  * Compilation flags
    This has been corrected - gcc is now called with %{optflags}

  * Timestamps
    The -p option has been added to all %__install and %__cp commands.

  * Unneeded ldconfig call
    All %post/%postun scriptlets have been dropped

  * Too generic names
    All binaries except "mace4" and "prover9" are now in "/usr/lib/prover9/bin".
Comment 4 Mamoru TASAKA 2008-07-06 14:09:26 EDT
For 200805a-2:

* Namespace issue
  - Please fix for too generic names on man pages, too.
    (by the way, is it really needed to create all symlinks
     for man pages, too?)

* Documents
  - prove9-apps subpackage can be installed without prove9 package.
    In such case, documents like COPYING and so are not installed,
    which is wrong.
    At least some files should be moved to prove9-apps subpackage.

* rpmlint issue:
prover9-apps.i386: W: spurious-executable-perm
prover9-apps.i386: W: doc-file-dependency
/usr/share/doc/prover9-apps-200805a/apps.examples/run-all /bin/csh
prover9-devel.i386: W: spurious-executable-perm /usr/lib/libladr.a
  - run-all script has executable permission bits and this adds
    unneeded Requires (/bin/csh) to -apps subpackage.
    Please fix the permission to 0644.
  - Static archives should have 0644 permission.

* test
  - build.log shows
   284  /bin/cp -p utilities/* bin
   285  **** Now try 'make test1'. ****
    Would you consider to add %check section and do some tests there?
Comment 5 Tim Colles 2008-07-08 11:56:27 EDT
Thanks for the additional comments. The new release at:

  Spec URL: http://homepages.inf.ed.ac.uk/timc/prover9/prover9.spec
  SRPM URL: http://homepages.inf.ed.ac.uk/timc/prover9/prover9-200805a-3.src.rpm

fixes all these:

  * Namespace issue
    Binaries all now have a prover9- prefix (except mace4/prover9) and are
    back in /usr/bin. Man pages have been similarly renamed. This seems to
    be a cleaner way to do this (eg. like git package) than a sub-directory.
    Dropped most of the man page symlinks as not really necessary.

  * Documents
    This was a hangover from the previous version which created dynamic libs.
    Changed the dependency order so prover9-apps now requires prover9 instead
    of the other way around - this is then consistent with all the other

  * rpmlint issue
    Both permissions have been fixed and everything is now completely clean
    under rpmlint.

  * test
    Added a %check section to do all the tests.


Comment 7 Tim Colles 2008-07-09 09:11:59 EDT
Thanks for testing the package. The new release at:

  Spec URL: http://homepages.inf.ed.ac.uk/timc/prover9/prover9.spec
  SRPM URL: http://homepages.inf.ed.ac.uk/timc/prover9/prover9-200805a-4.src.rpm

explicitly excludes ppc64 architecture with a suitable comment.
Unfortunately I don't have access to a ppc64 machine to test/debug this
Comment 8 Mamoru TASAKA 2008-07-09 13:36:49 EDT
I will check your latest srpm later. By the way:

NOTE: Before being sponsored:

This package will be accepted with another few work. 
But before I accept this package, someone (I am a candidate) 
must sponsor you.

Once you are sponsored, you have the right to review other 
submitters' review requests and approve the packages formally. 
For this reason, the person who want to be sponsored (like you) 
are required to "show that you have an understanding 
of the process and of the packaging guidelines" as is described
on :

Usually there are two ways to show this.
A. submit other review requests with enough quality.
B. Do a "pre-review" of other person's review request
   (at the time you are not sponsored, you cannot do
   a formal review)

When you have submitted a new review request or have pre-reviewed other 
person's review request, please write the bug number on this bug report 
so that I can check your comments or review request.

Fedora package collection review requests which are waiting for someone to
review can be checked on:
(NOTE: please don't choose "Merge Review")

Review guidelines are described mainly on:
Comment 9 Mamoru TASAKA 2008-07-10 12:15:40 EDT
Okay, this package itself seems good now. So I will wait for your pre-review or
another review request.
Comment 10 Mamoru TASAKA 2008-07-18 11:18:12 EDT
Comment 11 Tim Colles 2008-07-21 08:52:35 EDT
Hi. Was on holiday last week :) Will get going with a pre-review and hopefully
another review request this week.
Comment 12 Tim Colles 2008-07-25 09:28:26 EDT
Hi. Have pre-reviewed a couple of random submissions. They are #456038 and
#454482. I am also still working on making one of my own packages compliant,
it is in for review (#428435) but I need to make some changes to the source
to make it acceptable - will be getting back to this one in a short while.
Comment 13 Mamoru TASAKA 2008-07-25 14:56:44 EDT

+ I already said that this package itself is okay
+ Your pre-review is good for initial comments.

             This package (prove9) is APPROVED by me

Please follow the procedure written on:
from "Get a Fedora Account".
At a point a mail should be sent to sponsor members which notifies
that you need a sponsor. At the stage, please also write on
this bug for confirmation that you requested for sponsorship and
your FAS (Fedora Account System) name. Then I will sponsor you.

If you want to import this package into Fedora 8/9, you also have
to look at
(after once you rebuilt this package on koji Fedora rebuilding system).

If you have questions, please ask me.
Comment 14 Tim Colles 2008-07-30 09:32:21 EDT
Hi. I confirm that I am requesting sponsorship. My FAS name is "tcolles". Note
that on "http://fedoraproject.org/wiki/PackageMaintainers/Join" it says that you
need to apply to the "cvsextras" group which no longer seems to exist (the page
also has a broken link to that group). It looks to me like it should now be the
"packager" group, and that is the one I have applied for, perhaps the web page
could be updated (if I am correct).
Comment 15 Mamoru TASAKA 2008-07-30 10:22:18 EDT
Yes, cvsextras is renamed to packager.

By the way on FAS your email address information is lacking. Would you
update your FAS information?
Comment 16 Tim Colles 2008-07-30 10:32:57 EDT
It is there. Maybe because the account was marked private? Anyhow I have
unchecked that option to see if it makes any difference.
Comment 17 Mamoru TASAKA 2008-07-30 10:43:30 EDT
Okay, confirmed. Now I am sponsoring you. Please follow "Join" wiki
Comment 18 Tim Colles 2008-08-04 10:16:20 EDT
New Package CVS Request
Package Name: prover9
Short Description: Thereom Prover and Countermodel Generator
Owners: tcolles
Branches: F-9 EL-5
InitialCC: tcolles
Cvsextras Commits: yes
Comment 19 Kevin Fenzi 2008-08-04 14:45:36 EDT
cvs done.
Comment 20 Fedora Update System 2008-08-06 05:31:12 EDT
prover9-200805a-4.fc9 has been submitted as an update for Fedora 9
Comment 21 Mamoru TASAKA 2008-08-06 06:18:57 EDT
Comment 22 Fedora Update System 2008-08-07 19:51:29 EDT
prover9-200805a-4.fc9 has been pushed to the Fedora 9 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.