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.
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
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.
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
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.
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.
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
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
(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)
(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
(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
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.
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
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
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.
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.