Bug 459409 - Review Request: E - Equational Theorem Prover
Summary: Review Request: E - Equational Theorem Prover
Keywords:
Status: CLOSED NEXTRELEASE
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Richard W.M. Jones
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2008-08-18 16:15 UTC by David A. Wheeler
Modified: 2008-09-10 06:48 UTC (History)
3 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2008-09-05 12:20:23 UTC
Type: ---
Embargoed:
rjones: fedora-review+
kevin: fedora-cvs+


Attachments (Terms of Use)

Description David A. Wheeler 2008-08-18 16:15:19 UTC
Spec URL: http://www.dwheeler.com/E.spec
SRPM URL: http://www.dwheeler.com/E-0.999.006-1.fc9.src.rpm
Description:
E is a purely equational theorem prover for full first-order logic.
That means it is a program that you can stuff a mathematical specification
(in first-order format) and a hypothesis into, and which will then run
forever, using up all of your machines' resources.
Very occasionally it will find a proof for the hypothesis and tell you so.

E's inference core is based on a modified version of the superposition
calculus for equational clausal logic.  Both clausification and reasoning on
the clausal form can be documented in checkable proof objects. 

E was the best-performing open source software prover in the 2008
CADE ATP System Competition (CASC) in the FOF, CNF, and UEQ divisions.



NOTE: Normally I would use mock and koji to test the package,
to make sure that the BuildRequires: is correct and that it
compiled in other circumstances.  Unfortunately, due to the Fedora
infrastructure problems, I cannot do that right now.
It compiles for me, and I intend to test this with mock and koji
as soon as I can do so.  In the meantime, I'd love to hear other
comments about this package. That way, when the Fedora infrastructure
comes back up, this will be ready to go.

Comment 1 Jason Tibbitts 2008-08-20 18:56:40 UTC
Wow, this one builds with -O6!  Without performance data, this is pointless; the package should use the standard set of compile flags.

rpmlint says:
  E.x86_64: E: non-standard-executable-perm /usr/bin/eground 0775
  E.x86_64: E: non-standard-executable-perm /usr/bin/epclextract 0775
  E.x86_64: E: non-standard-executable-perm /usr/bin/eprover 0775
These shouldn't be group writable.

I note that the debuginfo package is devoid of source.  I suspect this is because it doesn't use the proper compilation flags (mainly -g).

The package did build and install OK.  (I built it locally in mock.)

Comment 2 David A. Wheeler 2008-08-21 00:31:40 UTC
Excellent, thanks for the feedback.   I've resolved everything you mentioned, here's the new pair (any other comments?):

Spec URL: http://www.dwheeler.com/E.spec
SRPM URL: http://www.dwheeler.com/E-0.999.006-2.fc9.src.rpm

rpmlint reports no warnings or errors on i386.
I got mock to build this on an i386, and you reported on x86_64, so that's good news.  koji build --scratch isn't running, so I don't know about ppc or ppc64, though I have no reason to believe it _won't_ work.

Comment 3 David A. Wheeler 2008-08-25 18:31:56 UTC
Good news, I now have evidence that this package works on all architectures!

Koji is back up, and a scratch build with dist-f9 works on all supported architectures (i386, x86_64, ppc, ppc64).  Since this spec includes a %check script, this is evidence that the package really does work on all architectures.  Here's what I used:

$ koji build --scratch dist-f9 E-0.999.006-2.fc9.src.rpm 

...
  0 free  0 open  5 done  0 failed

Comment 4 David A. Wheeler 2008-08-25 21:46:53 UTC
Anyone willing to do a review?  Clean rpmlint, builds on all architectures.

Comment 5 David A. Wheeler 2008-08-25 21:47:35 UTC
(I'm hoping to get this in before the Fedora 10 "no more stuff" deadline arrives.)

Comment 6 Jason Tibbitts 2008-08-25 21:52:07 UTC
The Fedora 10 "no more stuff" deadline happens around the release of Fedora 12.  You have on the order of 15 months before that happens.

Comment 7 David A. Wheeler 2008-08-25 22:02:19 UTC
Regarding comment #6:
Fair enough; I meant I was hoping to beat the "Fedora 10 Beta freeze".  http://fedoraproject.org/wiki/Releases/10/Schedule  says that has already passed, but I suspect the infrastructure outage will mean some sort of extension.

Comment 8 Richard W.M. Jones 2008-08-25 22:22:19 UTC
I can probably pick this up tomorrow morning, but feel free to
review it before then if you want.

Comment 9 Richard W.M. Jones 2008-08-26 07:28:36 UTC
Taking bug for review ...

Comment 10 Richard W.M. Jones 2008-08-26 07:41:58 UTC
+ rpmlint output
  (no warnings or errors)
+ package name satisfies the packaging naming guidelines

  I'm a little dubious about calling the package 'E' rather
  than something like 'E-theorem-prover', but it doesn't
  seem to be specifically against any guideline.

+ specfile name matches the package base name
+ package should satisfy packaging guidelines
+ license meets guidelines and is acceptable to Fedora
  GPLv2
+ license matches the actual package license
+ %doc includes license file
+ spec file written in American English
+ spec file is legible
+ upstream sources match sources in the srpm
  5a2168d44e8b3f23f84ccc5ef66aadee 1324629
+ package successfully builds on at least one architecture
  i386, plus there is a Koji build
n/a ExcludeArch bugs filed
+ BuildRequires list all build dependencies
n/a %find_lang instead of %{_datadir}/locale/*
n/a binary RPM with shared library files must call ldconfig in %post and %postun
+ does not use Prefix: /usr
+ package owns all directories it creates
+ no duplicate files in %files
+ %defattr line
+ %clean contains rm -rf $RPM_BUILD_ROOT
+ consistent use of macros
+ package must contain code or permissible content
n/a large documentation files should go in -doc subpackage
+ files marked %doc should not affect package
n/a header files should be in -devel
n/a static libraries should be in -static
n/a packages containing pkgconfig (.pc) files need 'Requires: pkgconfig'
n/a libfoo.so must go in -devel
n/a -devel must require the fully versioned base
n/a packages should not contain libtool .la files
n/a packages containing GUI apps must include %{name}.desktop file
+ packages must not own files or directories owned by other packages
+ %install must start with rm -rf %{buildroot} etc.
+ filenames must be valid UTF-8

Optional:

n/a if there is no license file, packager should query upstream
n/a translations of description and summary for non-English languages, if available
- reviewer should build the package in mock
- the package should build into binary RPMs on all supported architectures
? review should test the package functions as described
n/a scriptlets should be sane
n/a pkgconfig files should go in -devel
+ shouldn't have file dependencies outside /etc /bin /sbin /usr/bin or /usr/sbin

===>>>  APPROVED  <<<===

Comment 11 David A. Wheeler 2008-08-26 20:31:03 UTC
Wow! Thanks for the quick turnaround!

>  I'm a little dubious about calling the package 'E' rather
> than something like 'E-theorem-prover', but it doesn't
> seem to be specifically against any guideline.

I wondered about that too, but they're consistent in their use of this unusual one-capital-letter name ("E").  There's even precedence for this - "R" is one of the most popular statistical packages, and the Fedora package name is, unsurprisingly, "R".  So, since they consistently use the name, there's no guideline against it, and we have precedent, I just went along with the flow.  Only 24 to go in U.S. ASCII :-).

Comment 12 David A. Wheeler 2008-08-26 20:37:20 UTC
New Package CVS Request
=======================
Package Name: E
Short Description: Equational Theorem Prover
Owners: dwheeler
Branches: F-8 F-9
InitialCC:

Comment 13 Kevin Fenzi 2008-08-26 23:30:31 UTC
cvs done.

Comment 14 David A. Wheeler 2008-08-27 00:20:47 UTC
Help! Can't build; is the build env still down?
I got the cvs directories okay, but can't seem to build for F-8, F-9,
_OR_ devel. I just get these errors:
"FAILED: BuildError: package E not in list for tag dist-f8-updates-candidate"



I ran this:
 cd ~/cvs
 fedora-cvs E
 cd E
 ./common/cvs-import.sh ~/dwheeler.com/E-0.999.006-2.fc9.src.rpm 
 ./common/cvs-import.sh -b F-9 ~/dwheeler.com/E-0.999.006-2.fc9.src.rpm 
 ./common/cvs-import.sh -b F-8 ~/dwheeler.com/E-0.999.006-2.fc9.src.rpm 
 cd F-8
 cvs up
 cd ../F-9
 cvs up
 cd ../devel/
 cvs up
 cd ..
 cd F-8
 make build
 cd ../F-9/
 make build
 cd ../devel/
 make build


Here's what I get (skipping to the "make build" stuff):

$ cd F-8
$ make build
/usr/bin/koji  build  dist-f8-updates-candidate 'cvs://cvs.fedoraproject.org/cvs/pkgs?rpms/E/F-8#E-0_999_006-2_fc8'
Created task: 787924
Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=787924
Watching tasks (this may be safely interrupted)...
787924 build (dist-f8-updates-candidate, F-8:E-0_999_006-2_fc8): free
787924 build (dist-f8-updates-candidate, F-8:E-0_999_006-2_fc8): free -> open (ppc4.fedora.phx.redhat.com)
  787925 buildSRPMFromSCM (F-8:E-0_999_006-2_fc8): free
  787925 buildSRPMFromSCM (F-8:E-0_999_006-2_fc8): free -> open (x86-7.fedora.phx.redhat.com)
  787925 buildSRPMFromSCM (F-8:E-0_999_006-2_fc8): open (x86-7.fedora.phx.redhat.com) -> closed
  0 free  1 open  1 done  0 failed
787924 build (dist-f8-updates-candidate, F-8:E-0_999_006-2_fc8): open (ppc4.fedora.phx.redhat.com) -> FAILED: BuildError: package E not in list for tag dist-f8-updates-candidate
  0 free  0 open  1 done  1 failed

787924 build (dist-f8-updates-candidate, F-8:E-0_999_006-2_fc8) failed
make: *** [koji] Error 1



$ cd ../F-9/
$ make build
/usr/bin/koji  build  dist-f9-updates-candidate 'cvs://cvs.fedoraproject.org/cvs/pkgs?rpms/E/F-9#E-0_999_006-2_fc9'
Created task: 787926
Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=787926
Watching tasks (this may be safely interrupted)...
787926 build (dist-f9-updates-candidate, F-9:E-0_999_006-2_fc9): free
787926 build (dist-f9-updates-candidate, F-9:E-0_999_006-2_fc9): free -> open (x86-3.fedora.phx.redhat.com)
  787927 buildSRPMFromSCM (F-9:E-0_999_006-2_fc9): free
  787927 buildSRPMFromSCM (F-9:E-0_999_006-2_fc9): free -> open (ppc2.fedora.redhat.com)
  787927 buildSRPMFromSCM (F-9:E-0_999_006-2_fc9): open (ppc2.fedora.redhat.com) -> closed
  0 free  1 open  1 done  0 failed
787926 build (dist-f9-updates-candidate, F-9:E-0_999_006-2_fc9): open (x86-3.fedora.phx.redhat.com) -> FAILED: BuildError: package E not in list for tag dist-f9-updates-candidate
  0 free  0 open  1 done  1 failed

787926 build (dist-f9-updates-candidate, F-9:E-0_999_006-2_fc9) failed
make: *** [koji] Error 1



$ cd ../devel/
$ make build
/usr/bin/koji  build  dist-f10 'cvs://cvs.fedoraproject.org/cvs/pkgs?rpms/E/devel#E-0_999_006-2_fc10'
Created task: 787928
Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=787928
Watching tasks (this may be safely interrupted)...
787928 build (dist-f10, devel:E-0_999_006-2_fc10): open (ppc4.fedora.phx.redhat.com)
  787929 buildSRPMFromSCM (devel:E-0_999_006-2_fc10): free
  787929 buildSRPMFromSCM (devel:E-0_999_006-2_fc10): free -> open (x86-5.fedora.phx.redhat.com)
  787929 buildSRPMFromSCM (devel:E-0_999_006-2_fc10): open (x86-5.fedora.phx.redhat.com) -> closed
  0 free  1 open  1 done  0 failed
787928 build (dist-f10, devel:E-0_999_006-2_fc10): open (ppc4.fedora.phx.redhat.com) -> FAILED: BuildError: package E not in list for tag dist-f10
  0 free  0 open  1 done  1 failed

787928 build (dist-f10, devel:E-0_999_006-2_fc10) failed
make: *** [koji] Error 1

Comment 15 Richard W.M. Jones 2008-08-27 07:25:41 UTC
I would suggest leaving it for a few hours.  Just because
Kevin posts his 'cvs done' message doesn't mean that all
databases have been updated and all cron jobs have run.

Comment 16 Fedora Update System 2008-08-28 15:21:10 UTC
E-0.999.006-2.fc8 has been submitted as an update for Fedora 8.
http://admin.fedoraproject.org/updates/E-0.999.006-2.fc8

Comment 17 Fedora Update System 2008-08-28 15:21:13 UTC
E-0.999.006-2.fc9 has been submitted as an update for Fedora 9.
http://admin.fedoraproject.org/updates/E-0.999.006-2.fc9

Comment 18 Fedora Update System 2008-09-05 12:20:19 UTC
E-0.999.006-2.fc8 has been pushed to the Fedora 8 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 19 Fedora Update System 2008-09-10 06:35:30 UTC
E-0.999.006-2.fc9 has been pushed to the Fedora 9 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 20 Fedora Update System 2008-09-10 06:48:38 UTC
E-0.999.006-2.fc8 has been pushed to the Fedora 8 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.