[Bug 460244] Review Request: alt-ergo - Alt-Ergo automatic theorem prover

Thu Aug 28 16:04:33 UTC 2008

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.

https://bugzilla.redhat.com/show_bug.cgi?id=460244

--- Comment #3 from David A. Wheeler <dwheeler at dwheeler.com>  2008-08-28 12:04:32 EDT ---
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

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.