Bug 460244 - Review Request: alt-ergo - Alt-Ergo automatic theorem prover
Summary: Review Request: alt-ergo - Alt-Ergo automatic 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: David A. Wheeler
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2008-08-27 00:09 UTC by Alan Dunn
Modified: 2008-09-11 17:14 UTC (History)
4 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2008-09-11 17:03:27 UTC
Type: ---
Embargoed:
dwheeler: fedora-review+
kevin: fedora-cvs+


Attachments (Terms of Use)

Description Alan Dunn 2008-08-27 00:09:24 UTC
Spec URL: http://www.duke.edu/~amd34/alt-ergo/alt-ergo.spec
SRPM URL: http://www.duke.edu/~amd34/alt-ergo/alt-ergo-0.8-2.fc9.src.rpm
Description:
Alt-Ergo is an automated theorem prover implemented in OCaml. It is
based on CC(X) - a congruence closure algorithm parameterized by an
equational theory X. This algorithm is reminiscent of the Shostak
algorithm. Currently CC(X) is instantiated by the theory of linear
arithmetics. Alt-Ergo also contains a home made SAT-solver and an
instantiation mechanism by which it fully supports quantifiers.

Comment 1 Alan Dunn 2008-08-27 00:15:14 UTC
Bugzilla was inoperative at the time that I originally produced this package, so I solicited a review by email (from David Wheeler, who will vouch for this).

He wrote:


* I could NOT rebuild on i386; it seems to fail on ocaml-ocamlgraph. Perhaps the ocaml-ocamlgraph I'm using is not the latest version, but in any case, I got this error: "Cannot find file graph.cmxa".  I rebuilt
http://www.duke.edu/~amd34/ocamlgraph/ocaml-ocamlgraph-0.99c-2.fc9.src.rpm to create ocaml-ocamlgraph, and it's true, there's no .cmxa file:
$ rpm -qil ocaml-ocamlgraph
...
/usr/lib/ocaml/ocamlgraph
/usr/lib/ocaml/ocamlgraph/META
/usr/lib/ocaml/ocamlgraph/graph.cma
/usr/lib/ocaml/ocamlgraph/graph.cmi
/usr/share/doc/ocaml-ocamlgraph-0.99c/LICENSE

...

which I fixed in version 2 by adding ocaml-ocamlgraph-devel to BuildRequires (it is not yet in the repositories, which implies that I can't really use mock)

* In "cp %{SOURCE1} %{SOURCE2} .", say "cp -p" instead.  You should try to keep the timestamps where you can.  Indeed, if you got these files from elsewhere, try to preserve THEIR timestamps.

which I also changed, and the following two comments

* The spec file says this, and I couldn't figure out what "->" meant;
 can you make it clearer by replacing "->" with the word(s) you mean?
 # Avoid a Makefile patch by just adding this empty file -> autoconf
 # doesn't complain (better than ignoring all status from configure)

* I think the "iconv" should be run during _build_, not _install_.
Also, you have 3 semicolon-separated commands on one line to invoke it,
which kindof hides the "iconv".  I'd prefer to have that as a sequence
of 3 commands on 3 lines.  I'm not big on cuddling multiple commands
on a line anyway, but this sequence hides the important command:
"mv CeCILL-C CeCILL-C.iso8859; iconv -f ISO-8859-1 -t UTF-8 < CeCILL-C.iso8859 > CeCILL-C; rm CeCILL-C.iso8859"

which I also changed. He then gave a "more formal review":

+ rpmlint output
 It outputs:
 alt-ergo.i386: W: invalid-license CeCILL-C
 But this is an error in rpmlint (CeCILL-C is a recent addition),
 already explained in the spec file

+ package name satisfies the packaging naming guidelines
+ specfile name matches the package base name
+ package should satisfy packaging guidelines
+ license meets guidelines and is acceptable to Fedora
 Yes.  CeCILL-C was just added to the acceptable list.
+ license matches the actual package license
+ %doc includes license file
  Yes, /usr/share/doc/alt-ergo-0.8/CeCILL-C
+ spec file written in American English
+ spec file is legible
+ upstream sources match sources in the srpm
 Yes, sha1sum:
 6a073b88d799e3dfcc7e13dfc1386c6422ce9ab8
+ package successfully builds on at least one architecture
 i386.  Can't try koji until ocamlgraph is in.
??? ExcludeArch bugs filed
??? BuildRequires list all build dependencies
 (Not yet)
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
 Don't know how to do that yet; ocamlgraph not available in yum
??? the package should build into binary RPMs on all supported architectures
 Don't know how to do that yet; ocamlgraph not available in yum
+ review should test the package functions as described
 Tried using gwhy; looks great!
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

Comment 2 David A. Wheeler 2008-08-27 00:29:26 UTC
For completeness, I'll vouch that comment #1 is an accurate copy of the emails I sent Alan Dunn while Bugzilla was down.

I'm looking forward to seeing the updated alt-ergo.

I'll make myself the reviewer; thanks for packaging alt-ergo.

Comment 3 David A. Wheeler 2008-08-28 16:04:32 UTC
Okay, here's a re-review of your all-new, ever-wonderful revision 2 :-).

Good news: I tried calling it from "gwhy" on the "binary_search.c" test
file, and alt-ergo does REMARKABLY well.  It solved 30/31 (~97%) of the
verification conditions automatically! Since I was hoping for a
COMBINED score of 90% or more, that is GREAT.

Bad news: It fails to build on some architectures, nor does it exclude them.
See koji report below.

All my original top-level comments have been addressed:
* Rebuild now works (ocaml-ocamlgraph became ocaml-ocamlgraph-devel)
* "cp %{SOURCE1} %{SOURCE2} ." had "-p" added, good.
* Clarified comment
* iconv on own line

Formal review:

+ rpmlint output
 It outputs:
 alt-ergo.i386: W: invalid-license CeCILL-C
 But this is an error in rpmlint (CeCILL-C is a recent addition),
 already explained in the spec file.

 I confirmed that CeCILL-C is an approved Fedora license as noted here:
 http://fedoraproject.org/wiki/Licensing
 NOTE: CeCILL-C is _NOT_ the same as CeCILL.

+ package name satisfies the packaging naming guidelines
+ specfile name matches the package base name
+ package should satisfy packaging guidelines
+ license meets guidelines and is acceptable to Fedora
 Yes.  CeCILL-C was just added to the acceptable list.
+ license matches the actual package license
+ %doc includes license file
  Yes, /usr/share/doc/alt-ergo-0.8/CeCILL-C
+ spec file written in American English
+ spec file is legible
+ upstream sources match sources in the srpm
 Yes, sha1sum:
 6a073b88d799e3dfcc7e13dfc1386c6422ce9ab8
+ package successfully builds on at least one architecture
 Confirmed i386 works.
 Previously, couldn't easily test koji until ocamlgraph is in
 the repository (and Fedora infrastructure had lots of problems too).
 I also tried:
  koji build --scratch alt-ergo-0.8-2.fc9.src.rpm 

-FAIL ExcludeArch bugs filed
+ BuildRequires list all build dependencies
  Does now (that was a fix from revision 1. Alan Dunn could not
  easily test for this when he created revision 1, because of
  Fedora's infrastructure problems combined with the lack of ocamlgraph.)
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
 Used koji, which uses mock.
-FAIL the package should build into binary RPMs on all supported architectures
+ review should test the package functions as described
 Tried using gwhy; looks great!
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



$ koji build --scratch dist-f9 alt-ergo-0.8-2.fc9.src.rpm

Uploading srpm: alt-ergo-0.8-2.fc9.src.rpm
[====================================] 100% 00:00:02 114.05 KiB  46.40 KiB/sec
Created task: 790529
Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=790529
Watching tasks (this may be safely interrupted)...
790529 build (dist-f9, alt-ergo-0.8-2.fc9.src.rpm): free
790529 build (dist-f9, alt-ergo-0.8-2.fc9.src.rpm): free -> open (x86-3.fedora.phx.redhat.com)
  790532 buildArch (alt-ergo-0.8-2.fc9.src.rpm, ppc): free
  790533 buildArch (alt-ergo-0.8-2.fc9.src.rpm, x86_64): free
  790534 buildArch (alt-ergo-0.8-2.fc9.src.rpm, i386): free
  790535 buildArch (alt-ergo-0.8-2.fc9.src.rpm, ppc64): open (ppc4.fedora.phx.redhat.com)
  790532 buildArch (alt-ergo-0.8-2.fc9.src.rpm, ppc): free -> open (ppc10.fedora.phx.redhat.com)
  790533 buildArch (alt-ergo-0.8-2.fc9.src.rpm, x86_64): free -> open (xenbuilder4.fedora.phx.redhat.com)
  790534 buildArch (alt-ergo-0.8-2.fc9.src.rpm, i386): free -> open (x86-2.fedora.phx.redhat.com)
  790534 buildArch (alt-ergo-0.8-2.fc9.src.rpm, i386): open (x86-2.fedora.phx.redhat.com) -> FAILED: BuildrootError: error building package (arch i386), mock exited with status 10
  0 free  4 open  0 done  1 failed
  790533 buildArch (alt-ergo-0.8-2.fc9.src.rpm, x86_64): open (xenbuilder4.fedora.phx.redhat.com) -> FAILED: BuildrootError: error building package (arch x86_64), mock exited with status 10
  0 free  3 open  0 done  2 failed
  790535 buildArch (alt-ergo-0.8-2.fc9.src.rpm, ppc64): open (ppc4.fedora.phx.redhat.com) -> canceled
  0 free  2 open  1 done  2 failed
790529 build (dist-f9, alt-ergo-0.8-2.fc9.src.rpm): open (x86-3.fedora.phx.redhat.com) -> FAILED: BuildrootError: error building package (arch i386), mock exited with status 10
  0 free  1 open  1 done  3 failed
  790532 buildArch (alt-ergo-0.8-2.fc9.src.rpm, ppc): open (ppc10.fedora.phx.redhat.com) -> canceled
  0 free  0 open  2 done  3 failed

Comment 4 David A. Wheeler 2008-08-28 17:55:05 UTC
Oops! I misunderstood the koji error messages.  I thought that ocaml-ocamlgraph had been pushed out, but it appears that it has _NOT_ been pushed out.  So, unsurprisingly, those builds fail.

On my system, once ocaml-ocamlgraph is installed, it works just fine.

So the builds on the other architectures _should_ work, but I cannot confirm that.
I see that ocaml-ocamlgraph has been built:
http://koji.fedoraproject.org/koji/buildinfo?buildID=59965
and that it's pending at bodhi:
https://admin.fedoraproject.org/updates/ocaml-ocamlgraph-0.99c-2.fc9

ocaml-ocamlgraph was submitted on 08-23 (5 days ago).  The easy solution is to wait for Bodhi to post it, so that the other tests will be easy to do.  I don't want to wait forever, though; if this package is ready (and I suspect it is), I'd like to see this in the repository before the F10 freeze.

Comment 5 David A. Wheeler 2008-09-04 15:21:15 UTC
Okay, my review above was based on a misunderstanding.  Basically, the Fedora infrastructure problems are causing all sorts of nasty problems.  Package ocaml-ocamlgraph is required, and it's already approved and submitted to Bodhi, but it's not actually in the repository because everything is still frozen from the infrastructure problems.  *Sigh*.

This package builds cleanly on my system, so it clearly works on _an_ architecture.  I have no reason to believe it would fail on others, and even if it did, that wouldn't cause the package to be unacceptable. So under the formal review of the _required_ items, this changes to:
n/a ExcludeArch bugs filed

The other items are all optional.  I have every reason to believe that they will succeed once koji and Bodhi are fully operational, but since they are _optional_, they're not reasons to fail the package.

Basically, this _package_ is ready... the problem is that the Fedora _infrastructure_ is not ready.  So I will approve the package, which will permit setting up the CVS packages.  It won't build until Bodhi releases get unfrozen (due to the dependencies), but once the Bodhi infrastructure is fully working again, it'll work.

APPROVED.

Comment 6 Alan Dunn 2008-09-04 15:32:08 UTC
New Package CVS Request
=======================
Package Name: alt-ergo
Short Description: Alt-Ergo automatic theorem prover
Owners: amdunn
Branches: F-8 F-9
InitialCC:
Packager Commits: yes

Comment 7 Kevin Fenzi 2008-09-05 16:50:28 UTC
You should be able to build/test this against rawhide however, right? 

I fired off a scratch build against rawhide and it failed: 
http://koji.fedoraproject.org/koji/taskinfo?taskID=808966

Comment 8 Alan Dunn 2008-09-05 17:09:48 UTC
(In reply to comment #7)
> You should be able to build/test this against rawhide however, right? 
> 
> I fired off a scratch build against rawhide and it failed: 
> http://koji.fedoraproject.org/koji/taskinfo?taskID=808966

You are correct on both counts (should've realize re: rawhide for testing, but it's not a "full substitute" I suppose...) - was missing prelink from BuildRequires:

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

New SRPM and spec file at
http://www.duke.edu/~amd34/alt-ergo/

(or take from Koji)

Comment 9 David A. Wheeler 2008-09-05 19:03:08 UTC
(In reply to comment #7 and comment #8)

Kevin Fenzi: Thanks, you're absolutely right, that's a good work-around for the Fedora infrastructure problems.  Hopefully soon the Fedora infrastructure will actually "work as documented" :-).  I will try to revise the Fedora Wiki to note this work-around!!

Alan Dunn: Thanks for fixing the problem noted by Kevin Fenzi (once Fenzi noted the test work-around).

I took the revised SRPM posted in comment #8, and did:
  $ koji build --scratch dist-f10 alt-ergo-0.8-3.fc9.src.rpm
It worked fine on all architectures:
  0 free  0 open  5 done  0 failed

I rebuilt on my own system; it built fine. rpmlint has only one complaint about the spec and binary RPM:
 alt-ergo.i386: W: invalid-license CeCILL-C
which is no problem; CeCILL-C was recently added to the Fedora license list and rpmlint just hasn't been updated yet.

So, this revision is:
APPROVED

Comment 10 David A. Wheeler 2008-09-05 19:04:13 UTC
(To be nice to CVS maintainers, I'm repeating the CVS request so it's "at the bottom")


New Package CVS Request
=======================
Package Name: alt-ergo
Short Description: Alt-Ergo automatic theorem prover
Owners: amdunn
Branches: F-8 F-9
InitialCC:
Packager Commits: yes

Comment 11 Kevin Fenzi 2008-09-05 21:05:26 UTC
cvs done.

Note: 

> Kevin Fenzi: Thanks, you're absolutely right, that's a good work-around for the
> Fedora infrastructure problems.  Hopefully soon the Fedora infrastructure will
> actually "work as documented" :-).  I will try to revise the Fedora Wiki to
> note this work-around!!

This is not a problem, this is how it's supposed to work. 
In release branches (f8/f9 currently) builds are only done against the base gold repo + stable updates. Updates in updates-testing or updates that have not yet been pushed are not added to the buildroot. This is to prevent some update happening that depends on another package that is not pushed. 

If you need to build against a package that is not yet a stable released update, you can file a ticket with rel-eng at: https://fedorahosted.org/rel-eng/newticket and request that that package be added as a buildroot override.

Comment 12 Fedora Update System 2008-09-06 02:09:48 UTC
alt-ergo-0.8-3.fc9 has been submitted as an update for Fedora 9.
http://admin.fedoraproject.org/updates/alt-ergo-0.8-3.fc9

Comment 13 Fedora Update System 2008-09-06 02:11:02 UTC
alt-ergo-0.8-3.fc8 has been submitted as an update for Fedora 8.
http://admin.fedoraproject.org/updates/alt-ergo-0.8-3.fc8

Comment 14 Fedora Update System 2008-09-11 17:03:23 UTC
alt-ergo-0.8-3.fc9 has been pushed to the Fedora 9 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 15 Fedora Update System 2008-09-11 17:14:09 UTC
alt-ergo-0.8-3.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.