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) Description: 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.
*** Bug 428410 has been marked as a duplicate of this bug. ***
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: https://fedoraproject.org/wiki/PatriceDumas So if this package only provides static archives by default, please follow http://fedoraproject.org/wiki/Packaging/Guidelines#Packaging_Static_Libraries of "static libraries only". * Compilation flags - This package completely ignores Fedora specific compilation flags: http://fedoraproject.org/wiki/Packaging/Guidelines#Compiler_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?
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".
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 /usr/share/doc/prover9-apps-200805a/apps.examples/run-all 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?
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 sub-packages. * 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.
Test fails only on ppc64???? http://koji.fedoraproject.org/koji/taskinfo?taskID=703026 http://koji.fedoraproject.org/koji/taskinfo?taskID=703051
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 architecture.
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 : http://fedoraproject.org/wiki/PackageMaintainers/HowToGetSponsored 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: http://fedoraproject.org/PackageReviewStatus/NEW.html (NOTE: please don't choose "Merge Review") Review guidelines are described mainly on: http://fedoraproject.org/wiki/Packaging/ReviewGuidelines http://fedoraproject.org/wiki/Packaging/Guidelines http://fedoraproject.org/wiki/Packaging/ScriptletSnippets ------------------------------------------------------------
Okay, this package itself seems good now. So I will wait for your pre-review or another review request.
ping?
Hi. Was on holiday last week :) Will get going with a pre-review and hopefully another review request this week.
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.
Okay. + 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: http://fedoraproject.org/wiki/PackageMaintainers/Join 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 http://fedoraproject.org/wiki/Infrastructure/UpdatesSystem/Bodhi-info-DRAFT (after once you rebuilt this package on koji Fedora rebuilding system). If you have questions, please ask me.
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).
Yes, cvsextras is renamed to packager. By the way on FAS your email address information is lacking. Would you update your FAS information?
It is there. Maybe because the account was marked private? Anyhow I have unchecked that option to see if it makes any difference.
Okay, confirmed. Now I am sponsoring you. Please follow "Join" wiki again.
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
cvs done.
prover9-200805a-4.fc9 has been submitted as an update for Fedora 9
Closing.
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.