Bug 453503 - Review Request:zenon - Automated theorem prover for first-order classical logic
Summary: Review Request:zenon - Automated theorem prover for first-order classical logic
Keywords:
Status: CLOSED CURRENTRELEASE
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Alan Dunn
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2008-07-01 03:43 UTC by David A. Wheeler
Modified: 2008-07-23 07:18 UTC (History)
2 users (show)

Fixed In Version: 0.5.0-2.1.fc8
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2008-07-23 07:08:14 UTC
Type: ---
Embargoed:
amdunn: fedora-review+
kevin: fedora-cvs+


Attachments (Terms of Use)

Description David A. Wheeler 2008-07-01 03:43:09 UTC
Spec URL: http://www.dwheeler.com/zenon.spec
SRPM URL: http://www.dwheeler.com/zenon-0.5.0-1.fc9.src.rpm
Description:
Zenon is an automated theorem prover for first order classical logic
with equality, based on the tableau method.
Zenon can read input files in TPTP, Coq, Focal, and its own Zenon format.
Zenon can directly generate Coq proofs (proof scripts or proof terms),
which can be reinserted into Coq specifications.
Zenon can also be extended.


================================================

* CLean rpmlint (.spec/.rpm/.src.rpm)
* Clean koji build for all f9 archs
* Open source software license (BSD)
* Meets all guidelines (to the best of my knowledge)

Comment 1 Alan Dunn 2008-07-09 03:45:31 UTC
This seems to meet all of the review criteria (though perhaps this should be
made even more extensive):

- Content permissible
- Name is proper
- No large documentation, documentation not needed to run (though thanks to you
it has more than none)
- No file types that should be moved to -devel or -static
(- No gui program)
- Proper file ownership
- rm -rf %{buildroot} run
- All filenames valid UTF-8

should items:
- License included and matches type indicated
- Package contains test (the tptp test for the halting problem)

Furthermore:

Package indeed builds in mock. I also tested a common need for ocaml packages: I
moved ocamlopt, ocamlopt.opt and tried a build. This works (the tptp test runs)
and produces the (expectedly slower) bytecode verion. Rpmlint is silent on
source RPM and produced binary RPM for opt build i386, though it makes a weird
claim for the bytecode version:

zenon.i386: E: no-binary
The package should be of the noarch architecture because it doesn't contain
any binaries.

This is not true from what I can tell, but probably indicated since the file
type of zenon is not ELF but the file command gives "zenon: a /usr/bin/ocamlrun
script text executable" (though it is a binary file, and I am under the
impression that this file is not architecture independent)

Koji builds for f9 as I see from

http://koji.fedoraproject.org/koji/taskinfo?taskID=688986

for example, though perhaps should be attempted for f10.

Only one real recommendation I see at the moment, which is relatively minor: I
would move tptp-COM003+2.p out of %doc - it's not really a documentation file,
it's a data (non-binary) file that probably just belongs in %{_datadir}.

Comment 2 David A. Wheeler 2008-07-09 04:10:56 UTC
Thanks for the review! Regarding questions/recommendations:

* I think the rpmlint result for the bytecode-only-version should be ignored.
  The problem is that rpmlint lacks context.  rpmlint can't realize that you
  would normally run a machine code version, and that the only reason that
  there's a bytecode version is because nothing better is available for
  that particular architecture.
* "perhaps should be attempted for f10." Ok, good point. I built for f10 using:
   koji build --scratch dist-f10 ../SRPMS/zenon-0.5.0-1.fc9.src.rpm
   and got 5 clean builds (no failures).
* "I would move tptp-COM003+2.p out of %doc - it's not really a
  documentation file, it's a data (non-binary) file that probably
  just belongs in %{_datadir}."  Hmm, I'm not sure how to respond to that.
  The reason I put it in %doc was because I was thinking of this test case
  as an example. It enables a human to understand (through example) how to
  use the program.  It's _not_ used during run-time (normally), e.g., it's
  not an architecture-independent library or anything like that.
  And this program has squat for documentation, so even an example
  is more than it had otherwise :-).
  I'd prefer to leave it in %doc, primarily because there's so little
  documentation that I'd rather give them SOMETHING to start.
  But I'm not hard over it.  Anyone else have any thoughts?



Comment 3 David A. Wheeler 2008-07-16 03:29:22 UTC
Since the Fedora guidelines don't say anything about where tests
or examples go, I went and looked the Debian guidelines, figuring
that if Debian preferred something and Fedora didn't care, it would be
convenient to users if Debian/Ubuntu and Fedora did the same thing.

I _thought_ that the Debian policy stated where to place test cases
if installed, but I didn't see anything when I went back to look.
But they DO have a recommended file placement scheme for examples. At:
  http://www.debian.org/doc/debian-policy/ch-docs.html#s12.6
Debian policies say:
"Any examples (configurations, source files, whatever), should be installed in a
directory /usr/share/doc/PACKAGE/examples. These files should not be referenced
by any program: they're there for the benefit of the system administrator and
users as documentation only."

So, instead of putting the example in /usr/share/doc/PACKAGENAME-VERSION/
(as done currently) _or_ in /usr/share/PACKAGENAME-VERSION/
(as Alan Dunn proposes), I propose placing the example
in /usr/share/doc/PACKAGENAME-VERSION/examples/
as required by the Debian guidelines (well, Debian doesn't add
"-VERSION" but that _is_ Fedora convention).  That way, if a Debian package
appears in the future, users will see a more consistent file location
scheme.  Granted, there aren't many examples now, but that at least
sets the stage for more examples later.  Given its lack of
documentation, SOMETHING as an example is better than nothing.

Sound reasonable?



Comment 4 Patrice Dumas 2008-07-16 08:13:26 UTC
(In reply to comment #3)
> Since the Fedora guidelines don't say anything about where tests
> or examples go, I went and looked the Debian guidelines, figuring
> that if Debian preferred something and Fedora didn't care, it would be
> convenient to users if Debian/Ubuntu and Fedora did the same thing.

There is no specific recommendation, except that, since it is some
documentation is should be in %doc.

> These files should not be referenced
> by any program: they're there for the benefit of the system administrator and
> users as documentation only."

That's in the guideline.

> in /usr/share/doc/PACKAGENAME-VERSION/examples/
> 
> Sound reasonable?

In general, the examples are indeed put in %doc examples/
or, if there are not so much files in %doc directly in %doc.
I don't think a formal guideline is needed, there are already a 
lot of guidelines. You could add it to 
http://fedoraproject.org/wiki/PackageMaintainers/PackagingTricks
however.

Comment 5 David A. Wheeler 2008-07-19 04:57:55 UTC
Okay, new version of the package, which takes into account everything above. 
Would someone re-review them?  They are here:
 http://www.dwheeler.com/zenon.spec
 http://www.dwheeler.com/zenon-0.5.0-2.fc9.src.rpm

rpmlint reports 0 errors and 0 warnings on the .spec, SRPM, and the built
i386 binary for fedora 9.  It builds for all architectures for both
dist-f9 and dist-f10.

It actually builds for dist-f8 too, for all but ppc64.
I modified my .spec file to account for this, but I believe there's
an error in the build system, so it tries to build on ppc64 anyway
(the dist-f8 seems to think that it's fedora 9 instead, e.g., %fedora == 9).
I've already posted a bug report on what I think is an infrastructure issue:
 https://fedorahosted.org/fedora-infrastructure/ticket/711
Since building for f8 isn't a requirement, I propose reviewing this
for Fedora 9 and rawhide.  If there's a build infrastructure bug, hopefully
it will get fixed. If the problem is a bug in my specfile, then I
can release that SRPM separately instead.

Alan Dunn:
>Only one real recommendation I see at the moment, which is relatively minor: I
>would move tptp-COM003+2.p out of %doc - it's not really a documentation file,
>it's a data (non-binary) file that probably just belongs in %{_datadir}.

I've moved it into an "examples" subdirectory of its %doc directory;
there are no Fedora rules about this, so I used the
Debian guidelines as I proposed (above).  I think it's a good idea
to follow guidelines from other distros if a given distro doesn't care..
makes things easier for everyone (and if the guideline gets copied, we're
ahead of the game).

Creating the examples/ subdirectory turns out to be
trickier than I expected, because the "%doc" macro auto-erases
anything in document subdirectories, so I also documented how to
do this in general here:
 http://fedoraproject.org/wiki/PackageMaintainers/PackagingTricks
as recommended by Patrice Dumas.




Comment 6 Alan Dunn 2008-07-20 09:58:53 UTC
Now that I can officially review (now sponsored) - will take this one and
upgrade the previous review as necessary.

Comment 7 Alan Dunn 2008-07-20 12:00:22 UTC
The slightly more extensive official review:

- rpmlint silent (well, except as mentioned above, but that's still ok to me)
- naming proper
- licensing ok (and included in %doc)
- specfile legible, in American English
- sources match upstream:
d5440999c6f92d436a1d1e96d4ffbd56  zenon-0.5.0.tar.gz
- successful build (tested on i386)
- no architecture blocking (on Fedora 9 and devel but see below)
- dependencies in BuildRequires
- proper file and directory ownership
- proper file attributes and defattr
- rm -rf %{buildroot} run in %clean
- no large docs/docs not required for running
- rm -rf %{buildroot} run at beginning of %install
- filenames valid UTF-8

shoulds:
- license in separate file (miswritten above in what I said)
- (no translations available for docs, but could eventually be by the
  team for French if docs are submitted back upstream)
- package still builds in mock
- package compiles for all architectures (again, see below)
- program runs (example works)

It seems like the ppc64 issue is actually resolved in that from the
discussion at

https://fedorahosted.org/fedora-infrastructure/ticket/711

I gather that for Koji scratch builds one needs to define the fedora
macro manually, but for "make build" builds, the macro is defined
properly in a rebuilding of the SRPM.

(Though technically I would've done a 0%{fedora} < 9 since this won't
work for Fedora 7, but that's probably going to be ok.)

So you could submit this for Fedora 8, but I suppose then you should
include the proper bug report.

Looks like you fixed what I wanted re: examples.

So:
APPROVED.

Comment 8 David A. Wheeler 2008-07-20 20:27:41 UTC
New Package CVS Request
=======================
Package Name: zenon
Short Description: Automated theorem prover for first-order classical logic
Owners: dwheeler
Branches: F-8 F-9
InitialCC: pertusus
Cvsextras Commits: yes


Comment 9 Kevin Fenzi 2008-07-21 16:02:29 UTC
cvs done.

Comment 10 Fedora Update System 2008-07-21 18:22:30 UTC
zenon-0.5.0-2.fc9 has been submitted as an update for Fedora 9

Comment 11 Fedora Update System 2008-07-21 18:24:46 UTC
zenon-0.5.0-2.1.fc8 has been submitted as an update for Fedora 8

Comment 12 David A. Wheeler 2008-07-21 20:36:59 UTC
I have submitted zenon for Fedora 8, Fedora 9, and Fedora 10/Rawhide.  I've set
Bodhi so that it'll be pushed out for Fedora 8 and Fedora 9.

One odd thing: I had to make a patch for Fedora 8. I used this construct:
 %{?fc8:ExcludeArch: ppc64}
which is one of the suggested formats documented in:
https://fedoraproject.org/wiki/Packaging/DistTag

Unfortunately, %fc8 didn't work. Instead, I had to do this:
 %if 0%fedora == 8
 ExcludeArch: ppc64
 %endif

I reported the problem with %fc8 as fedora-infrastructure ticket #717:
 https://fedorahosted.org/fedora-infrastructure/ticket/717
the infrastructure team have since fixed this, so %fc8 should work in the future.

I couldn't easily discover this earlier, because scratch builds across different
fedora releases don't work.  As noted in:
 https://fedorahosted.org/fedora-infrastructure/ticket/711
the values of %fedora, %fc8, etc., are determined by the CREATOR of the SRPM,
and NOT by the environment performing the build, so you effectively can't do
scratch builds for a different version of fedora than the one creating the SRPM.

Anyway, it's all posted, and a bug in the infrastructure has now been fixed so
future releases should go smoothly.


Comment 13 David A. Wheeler 2008-07-22 15:14:56 UTC
According to Bodhi:
 https://admin.fedoraproject.org/updates

Zenon has just been pushed to Fedora 9 (though mirrors may not have it yet):
 https://admin.fedoraproject.org/updates/F9/FEDORA-2008-6572

Zenon for Fedora 8 is pending, hopefully that will be out soon:
 https://admin.fedoraproject.org/updates/F8/pending/zenon-0.5.0-2.1.fc8



Comment 14 Fedora Update System 2008-07-23 07:08:11 UTC
zenon-0.5.0-2.1.fc8 has been pushed to the Fedora 8 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 15 Fedora Update System 2008-07-23 07:18:14 UTC
zenon-0.5.0-2.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.