Spec URL: http://jjames.fedorapeople.org/cvc3/cvc3.spec SRPM URL: http://jjames.fedorapeople.org/cvc3/cvc3-2.1-1.fc11.src.rpm Description: CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
I'm looking through it right now. Here are a few quick comments, a more formal review to come. It looks like the license problems are completely gone!! I double-checked the main license in LICENSE.in; the nasty non-BSD clause originally there (aka the "pay up if I get sued" clause) is gone. Hooray!! The LICENSE.in file gives a short list of files with different licenses; I looked at every one of those files, and they're clearly BSD-style as well. CVC3 version 1.2 had zchaff, which could be removed; this version of CVC3 doesn't even INCLUDE zchaff as far as I can tell, so there aren't any zchaff licensing issues either. So happily, it looks like the licensing problems are completely gone. Excellent! This package doesn't enable the Java interface (--enable-java). At first, I thought that was unfortunate, but then I noticed that the documentation says that the interface is "experimental" and "may change". So, you might want to consider enabling the interface, but given that description, perhaps it's just as well. Java apps can always use the command-line interface anyway. I know of no rule forbidding the use of "%makeinstall". The rule, as I understand it, is that you should NOT use %makeinstall if "make DESTDIR=..." works. But DESTDIR isn't supported by CVC3's makefile, so that rule doesn't apply. So I think the %%makefile comment is misleading, but directly invoking make (as you've done) is okay. For more info, see: http://fedoraproject.org/wiki/Packaging/Guidelines#Why_the_.25makeinstall_macro_should_not_be_used
I just built the package; I have an rpmlint error, as well as several warnings. I think you HAVE to fix the rpmlint error, at least. So, here's what I've found so far in my review: An "rpmlint cvc3.spec" works just fine: 0 packages and 1 specfiles checked; 0 errors, 0 warnings. But when I built in on a 32-bit "i586" system and did rpmlint, I got this: $ rpmlint ../RPMS/i586/cvc3-*.rpm ../SRPMS/cvc3-2.1-1.fc11.src.rpm cvc3.i586: W: unstripped-binary-or-object /usr/lib/libcvc3.so.1.0.0 cvc3.i586: W: shared-lib-calls-exit /usr/lib/libcvc3.so.1.0.0 exit cvc3.i586: W: shared-lib-calls-exit /usr/lib/libcvc3.so.1.0.0 exit@@GLIBC_2.0 cvc3-devel.i586: E: zero-length /usr/share/doc/cvc3-devel-2.1/html/classHash_1_1hash__table__inherit__graph.png cvc3-emacs.i586: W: no-documentation cvc3-emacs-el.i586: W: no-documentation cvc3-xemacs.i586: W: no-documentation cvc3-xemacs-el.i586: W: no-documentation 8 packages and 0 specfiles checked; 1 errors, 7 warnings. The error is "zero-length /usr/share/doc/cvc3-devel-2.1/html/classHash_1_1hash__table__inherit__graph.png". This is merely in a missing figure in the *documentation*, not in the executing program, so it's not a crisis. It'd be nice if you could make sure it generates into a real graph, but if that fails, you should "remove this file if length is zero" since it's not supposed to have rpmlint errors. The "unstripped-binary-or-object" warning is odd; shouldn't that info have been moved into "cvc3-debuginfo"? The rest are probably non-events. The 4 'no-documentation' warnings are probably irrelevant, since the documentation presumably was put in the "cvc3-doc" package. I don't have a problem with shared libraries calling exit, unless users were expecting something else, so I don't think that's an issue either. I noticed some warnings during compilation, though that's depressingly common nowadays. When running doxygen, I noticed these: Generating docs for page INSTALL... /home/dwheeler/rpmbuild/BUILD/cvc3-2.1/INSTALL:198: Error: Unexpected character `"' ... Generating dependency graph for group ExprPkg /home/dwheeler/rpmbuild/BUILD/cvc3-2.1/src/include/expr.h:392: Error: Unexpected character `"' I'm wondering if these expressions are causing it trouble: "debug) contains the condition "f" Also, there's are 'useless rule' warnings from bison: bison -d -y -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y conflicts: 3 shift/reduce PL.y:1531.24-1536.25: warning: rule useless in parser due to conflicts: AndExpr: AndExpr "AND" Expr PL.y:1549.25-1554.25: warning: rule useless in parser due to conflicts: OrExpr: OrExpr "OR" Expr I did a quick trial run, and it seems to work correctly: cd ~/rpmbuild/BUILD/cvc3-2.1 LD_LIBRARY_PATH=`pwd`/lib bin/cvc3 +int CVC> i, j: INT; ASSERT i = j + 1; QUERY i>j; Valid. CVC> QUERY i<j; COUNTERMODEL; Invalid. Current scope level is 8. %Satisfiable Variable Assignment: % ASSERT (i = 0); ASSERT (j = -1); It'd be *nice* (though it's not required) if this had a %check section for automatic regression testing, e.g., something like: %check LD_LIBRARY_PATH=`pwd`/lib make regress4
Here's my initial review, per http://fedoraproject.org/wiki/Packaging:ReviewGuidelines In particular, I think you should consider having a separate "cvc3-doc" package instead of including it in cvc3-devel. The html documentation is HUGE, and I can easily see cases where (1) people want the docs but not the .h files, and (2) people want the .h files but not the docs. # MUST: rpmlint must be run on every package. The output should be posted in the review.[1] It has rpmlint warnings and errors; see my comments above. # MUST: The package must be named according to the Package Naming Guidelines . OK # MUST: The spec file name must match the base package %{name}, in the format %{name}.spec unless your package has an exemption. [2] . OK # MUST: The package must meet the Packaging Guidelines . I *think* so, other than the stuff noted above, but I have a question relating to minisat. It includes some "minisat" files; should it be referring to the minisat2 libraries instead? Or, would that not be appropriate? (I can easily believe that the minisat files in *this* program are not compatible, e.g., perhaps they're a fork from minisat2 or even the older minisat program). # MUST: The package must be licensed with a Fedora approved license and meet the Licensing Guidelines . OK. This was the problem originally. # MUST: The License field in the package spec file must match the actual license. [3] OK # MUST: If (and only if) the source package includes the text of the license(s) in its own file, then that file, containing the text of the license(s) for the package must be included in %doc.[4] OK # MUST: The spec file must be written in American English. [5] OK # MUST: The spec file for the package MUST be legible. [6] OK # MUST: The sources used to build the package must match the upstream source, as provided in the spec URL. Reviewers should use md5sum for this task. If no upstream URL can be specified for this package, please see the Source URL Guidelines for how to deal with this. OK. $ sha256sum cvc3-2.1.tar.gz ~/rpmbuild/SOURCES/cvc3-2.1.tar.gz b401610136a6150778327fe0eb4e3040705115ea79c434578cd9514a5be45ba3 cvc3-2.1.tar.gz b401610136a6150778327fe0eb4e3040705115ea79c434578cd9514a5be45ba3 /home/dwheeler/rpmbuild/SOURCES/cvc3-2.1.tar.gz # MUST: The package MUST successfully compile and build into binary rpms on at least one primary architecture. [7] OK. I used 32-bit i586. I also (briefly) installed and tried it out; seems to work. # MUST: If the package does not successfully compile, build or work on an architecture, then those architectures should be listed in the spec in ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in bugzilla, describing the reason that the package does not compile/build/work on that architecture. The bug number MUST be placed in a comment, next to the corresponding ExcludeArch line. [8] Don't know of any. You should use mock to try compiling on everything. # MUST: All build dependencies must be listed in BuildRequires, except for any that are listed in the exceptions section of the Packaging Guidelines ; inclusion of those as BuildRequires is optional. Apply common sense. OK. # MUST: The spec file MUST handle locales properly. This is done by using the %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.[9] NA # MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. [10] OK # MUST: Packages must NOT bundle copies of system libraries.[11] OK # MUST: If the package is designed to be relocatable, the packager must state this fact in the request for review, along with the rationalization for relocation of that specific package. Without this, use of Prefix: /usr is considered a blocker. [12] NA # MUST: A package must own all directories that it creates. If it does not create a directory that it uses, then it should require a package which does create that directory. [13] OK # MUST: A Fedora package must not list a file more than once in the spec file's %files listings. [14] OK # MUST: Permissions on files must be set properly. Executables should be set with executable permissions, for example. Every %files section must include a %defattr(...) line. [15] OK. # MUST: Each package must have a %clean section, which contains rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [16] OK # MUST: Each package must consistently use macros. [17] OK. "%{buildroot}" style used consistently. # MUST: The package must contain code, or permissable content. [18] OK. # MUST: Large documentation files must go in a -doc subpackage. (The definition of large is left up to the packager's best judgement, but is not restricted to size. Large can refer to either size or quantity). [19] No. As noted above, it's actually in -devel. I think the documentation should be in a cvc3-doc package instead. # MUST: If a package includes something as %doc, it must not affect the runtime of the application. To summarize: If it is in %doc, the program must run properly if it is not present. [19] OK # MUST: Header files must be in a -devel package. [20] OK # MUST: Static libraries must be in a -static package. [21] NA # MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for directory ownership and usability). [22] NA, no ".pc" files. # MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1), then library files that end in .so (without suffix) must go in a -devel package. [20] OK # MUST: In the vast majority of cases, devel packages must require the base package using a fully versioned dependency: Requires: %{name} = %{version}-%{release} [23] OK # MUST: Packages must NOT contain any .la libtool archives, these must be removed in the spec if they are built.[21] NA # MUST: Packages containing GUI applications must include a %{name}.desktop file, and that file must be properly installed with desktop-file-install in the %install section. If you feel that your packaged GUI application does not need a .desktop file, you must put a comment in the spec file with your explanation. [24] NA # MUST: Packages must not own files or directories already owned by other packages. The rule of thumb here is that the first package to be installed should own the files or directories that other packages may rely upon. This means, for example, that no package in Fedora should ever share ownership with any of the files or directories owned by the filesystem or man package. If you feel that you have a good reason to own a file or directory that another package owns, then please present that at package review time. [25] OK # MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [26] OK # MUST: All filenames in rpm packages must be valid UTF-8. [27] OK, I think. I did an "rpmls" on the generated packages, and the filenames all look like normal ASCII filenames (and thus UTF-8).
New URLs: http://jjames.fedorapeople.org/cvc3/cvc3.spec http://jjames.fedorapeople.org/cvc3/cvc3-2.1-2.fc11.src.rpm I have made the following changes: - The Java code is now built (it required a little patching to get the JNI code to build). - The %makeinstall macro is now used. - The empty PNG is a result of dot segfaulting on some really big input. For now, I'm letting it segfault and just removing the empty file. Long term, I'll try to get dot to generate good input, or make doxygen stop asking dot to process that file. - The unstripped library was due to the .so file not having the executable bits turned on. This is now fixed. - The files with missing " symbols are patched, so doxygen no longer complains. - The API documentation is now in a separate -doc package. I am not going to touch the useless rule warnings generated by bison, as I'm not certain I can do so without damaging the grammar files. We should report this upstream and see if they can fix it, though. I initially added the %check section that you suggested. However, when I enabled Java support, %check stopped working because it couldn't find the JAR files. There's probably an easy fix for that, but I haven't had time to pursue it yet. The minisat code does appear to be related somehow to that in the minisat2 package, but it differs signficantly. The minisat2 package supplies only a binary, not a library, so I couldn't link with it in any case. Even if it did supply a library, I am uncertain of the significance of the differences between the two code bases. How do you suggest I proceed on this point?
The changes all sound great. I'll start reviewing soon. Regarding your questions/comments... * "I am not going to touch the useless rule warnings generated by bison, as I'm not certain I can do so without damaging the grammar files. We should report this upstream and see if they can fix it, though." Fair enough. It may just be a misleading error message. I think reporting it upstream is the right solution. * "I initially added the %check section that you suggested. However, when I enabled Java support, %check stopped working because it couldn't find the JAR files. There's probably an easy fix for that, but I haven't had time to pursue it yet." Okay. Don't worry about it; %check is optional. I *like* having %check sections, and I encourage them, but I have no leg to stand on for *requiring* them. If you want to try further, you might be able to use "make regressonly4" instead of "make regress4" in the %check section. * "The minisat code does appear to be related somehow to that in the minisat2 package, but it differs signficantly. The minisat2 package supplies only a binary, not a library, so I couldn't link with it in any case. Even if it did supply a library, I am uncertain of the significance of the differences between the two code bases. How do you suggest I proceed on this point?" As you noted earlier, the minisat code in cvc3 has a copyright date of 2006, but the minisat2 has a date of 2005, and there are many differences in what's there. In addition, the CVC3 minisat does not include lots of code that is in minisat2. I think that is clear evidence that what we have here is an internal fork and serious modification of minisat, for purpose of implementing CVC3. I think we should encourage the CVC3 author and minisat2 authors to converge in the future, if it makes sense for them to do so. But for the moment, I think we should package as it is... there's absolutely no evidence that this fork will ever heal, or even that it SHOULD. Fedora already packages other forks that are more egregious (xemacs vs. emacs)... in this case, it's not even clear that there SHOULD be a merger. I'll go review the updated spec; thanks for doing this!!
I've looked over the new .spec file. Two small nits: You'll need to submit the Java patch upstream, and document the date you did so. The spec currently says: # Fix Java build problems. This patch has not yet been sent upstream. Patch3: cvc3-java.patch I know you already knew that. :-) I would recommend changing this: rm -f doc/html/classHash_1_1hash__table__inherit__graph.png to something like: badfile="doc/html/classHash_1_1hash__table__inherit__graph.png" if [ -f "$badfile" -a ! -s "$badfile" ] ; then rm -f "$badfile" fi That way, if future doxygens are changed to handle this graph, re-building the package will make it work automatically.
The patch has been sent upstream and the date noted in the spec file. I made the "badfile" change you suggested. Also, the %check section is now there. It checks only the C++ interface. Due to Fedora's requirements on the placement of arch-specific JARs, I have to patch the Java sources to replace loadLibrary with load of an absolute path. This means that the JAR cannot be loaded until after it is installed, which prevents any checking. The URLs are the same as before: http://jjames.fedorapeople.org/cvc3/cvc3.spec http://jjames.fedorapeople.org/cvc3/cvc3-2.1-2.fc11.src.rpm
That's great news!!! I think we're getting really close, if not there, but I have two questions about the rpmlint output. Results of: rpmlint cvc3.spec cvc3.spec:98: W: non-standard-group Development/Libraries/Java 0 packages and 1 specfiles checked; 0 errors, 1 warnings. QUESTION 1: Is that the right group for a Java library? Results of: rpmlint ../RPMS/i586/cvc3-* cvc3.i586: W: shared-lib-calls-exit /usr/lib/libcvc3.so.1.0.0 exit cvc3-devel.i586: W: no-documentation cvc3-emacs.i586: W: no-documentation cvc3-emacs-el.i586: W: no-documentation cvc3-java.i586: W: non-standard-group Development/Libraries/Java cvc3-java.i586: W: no-documentation cvc3-java.i586: W: devel-file-in-non-devel-package /usr/lib/cvc3/libcvc3jni.so cvc3-xemacs.i586: W: no-documentation cvc3-xemacs-el.i586: W: no-documentation 9 packages and 0 specfiles checked; 0 errors, 9 warnings. Nearly all of these warnings are dups or non-problems. The "no-documentation" ones are fine (the docs are in the cvc3-doc package), and calling exit is fine as well. The "non-standard-group" is a duplicate warning, as noted above, so the same question applies. QUESTION 2: What about this warning, though - is that a problem?: cvc3-java.i586: W: devel-file-in-non-devel-package /usr/lib/cvc3/libcvc3jni.so Is this the right way to package a Java library? I would've expected this to be in a "java-devel" package; are my expectations incorrect? I haven't delved into the rules for Java packages. I looked at the rpmls output; that looked okay. I installed and did a few simple tests - they worked perfectly.
Regarding question 1, the group doesn't really matter. The tools that categorize software all work off of comps.xml. In any case, that particular group is used by a lot of Java software; e.g., avalon-logkit, axis, bcel, icu4j, jdom, velocity, ws-jaxme, etc. Regarding question 2, that is the shared object used by JNI to connect to the (C++) shared library for invoking native Java methods. It is not a development file; it is necessary for the Java interface to function. Rpmlint just thinks it is a development file because of the .so filename extension.
Here's my review, per http://fedoraproject.org/wiki/Packaging:ReviewGuidelines # MUST: rpmlint must be run on every package. The output should be posted in the review.[1] Done, see above. The rpmlint warnings are irrelevant. # MUST: The package must be named according to the Package Naming Guidelines . OK # MUST: The spec file name must match the base package %{name}, in the format %{name}.spec unless your package has an exemption. [2] . OK # MUST: The package must meet the Packaging Guidelines . OK # MUST: The package must be licensed with a Fedora approved license and meet the Licensing Guidelines . OK. This was the problem originally, and I'm SO glad it's fixed!! # MUST: The License field in the package spec file must match the actual license. [3] OK # MUST: If (and only if) the source package includes the text of the license(s) in its own file, then that file, containing the text of the license(s) for the package must be included in %doc.[4] OK # MUST: The spec file must be written in American English. [5] OK # MUST: The spec file for the package MUST be legible. [6] OK # MUST: The sources used to build the package must match the upstream source, as provided in the spec URL. Reviewers should use md5sum for this task. If no upstream URL can be specified for this package, please see the Source URL Guidelines for how to deal with this. OK. $ sha256sum cvc3-2.1.tar.gz ~/rpmbuild/SOURCES/cvc3-2.1.tar.gz b401610136a6150778327fe0eb4e3040705115ea79c434578cd9514a5be45ba3 cvc3-2.1.tar.gz b401610136a6150778327fe0eb4e3040705115ea79c434578cd9514a5be45ba3 /home/dwheeler/rpmbuild/SOURCES/cvc3-2.1.tar.gz # MUST: The package MUST successfully compile and build into binary rpms on at least one primary architecture. [7] OK. I used 32-bit i586. I also (briefly) installed and tried it out; seems to work. # MUST: If the package does not successfully compile, build or work on an architecture, then those architectures should be listed in the spec in ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in bugzilla, describing the reason that the package does not compile/build/work on that architecture. The bug number MUST be placed in a comment, next to the corresponding ExcludeArch line. [8] OK. I don't know of any architecture it fails on, and it DOES work on x86 32-bit. I'm not required to do mock builds. # MUST: All build dependencies must be listed in BuildRequires, except for any that are listed in the exceptions section of the Packaging Guidelines ; inclusion of those as BuildRequires is optional. Apply common sense. OK. # MUST: The spec file MUST handle locales properly. This is done by using the %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.[9] NA # MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. [10] OK # MUST: Packages must NOT bundle copies of system libraries.[11] OK # MUST: If the package is designed to be relocatable, the packager must state this fact in the request for review, along with the rationalization for relocation of that specific package. Without this, use of Prefix: /usr is considered a blocker. [12] NA # MUST: A package must own all directories that it creates. If it does not create a directory that it uses, then it should require a package which does create that directory. [13] OK # MUST: A Fedora package must not list a file more than once in the spec file's %files listings. [14] OK # MUST: Permissions on files must be set properly. Executables should be set with executable permissions, for example. Every %files section must include a %defattr(...) line. [15] OK. # MUST: Each package must have a %clean section, which contains rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [16] OK # MUST: Each package must consistently use macros. [17] OK. "%{buildroot}" style used consistently. # MUST: The package must contain code, or permissable content. [18] OK. # MUST: Large documentation files must go in a -doc subpackage. (The definition of large is left up to the packager's best judgement, but is not restricted to size. Large can refer to either size or quantity). [19] Yes. (This is a change from the earlier version of this package.) # MUST: If a package includes something as %doc, it must not affect the runtime of the application. To summarize: If it is in %doc, the program must run properly if it is not present. [19] OK # MUST: Header files must be in a -devel package. [20] OK # MUST: Static libraries must be in a -static package. [21] NA # MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for directory ownership and usability). [22] NA, no ".pc" files. # MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1), then library files that end in .so (without suffix) must go in a -devel package. [20] OK # MUST: In the vast majority of cases, devel packages must require the base package using a fully versioned dependency: Requires: %{name} = %{version}-%{release} [23] OK # MUST: Packages must NOT contain any .la libtool archives, these must be removed in the spec if they are built.[21] NA # MUST: Packages containing GUI applications must include a %{name}.desktop file, and that file must be properly installed with desktop-file-install in the %install section. If you feel that your packaged GUI application does not need a .desktop file, you must put a comment in the spec file with your explanation. [24] NA # MUST: Packages must not own files or directories already owned by other packages. The rule of thumb here is that the first package to be installed should own the files or directories that other packages may rely upon. This means, for example, that no package in Fedora should ever share ownership with any of the files or directories owned by the filesystem or man package. If you feel that you have a good reason to own a file or directory that another package owns, then please present that at package review time. [25] OK # MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [26] OK # MUST: All filenames in rpm packages must be valid UTF-8. [27] OK, I think. I did an "rpmls" on the generated packages, and the filenames all look like normal ASCII filenames (and thus UTF-8). APPROVED!!
Thanks, David. If you or any of your colleagues want to comaintain this package, just put in a packagedb request and I'll grant it. New Package CVS Request ======================= Package Name: cvc3 Short Description: Validity checker of many-sorted first-order formulas with theories Owners: jjames Branches: F-11 InitialCC:
cvs done with F-12 branch added.
cvc3-2.1-2.fc11 has been submitted as an update for Fedora 11. http://admin.fedoraproject.org/updates/cvc3-2.1-2.fc11
cvc3-2.1-2.fc11 has been pushed to the Fedora 11 stable repository. If problems still persist, please make note of it in this bug report.
I've just rebuilt this package without the huge doxygen class graph images. Easily acheived by simply nodep-ing the graphviz build dep. Resulting doc size: 3.9M cvc3-doc-2.1-2.fc12.x86_64.rpm , compared to what I can currently find in my mirror 403M development/i386/os/Packages/cvc3-doc-2.1-2.fc12.i686.rpm 403M development/x86_64/os/Packages/cvc3-doc-2.1-2.fc12.x86_64.rpm 426M updates/11/i386/cvc3-doc-2.1-2.fc11.i586.rpm 426M updates/11/x86_64/cvc3-doc-2.1-2.fc11.x86_64.rpm and these are all unique. No noarch, no hardlink possible. I don't know what you guys were thinking but no pretty doc graphs are worth that much global space. Please just drop the graphviz builddep.
cvc3-2.1-3.fc11 has been submitted as an update for Fedora 11. http://admin.fedoraproject.org/updates/cvc3-2.1-3.fc11
Yanko, sorry about that. The process of getting cvc3 to compile and working with upstream to resolve license issues took so much time and energy that I apparently lost focus at the end. I've fixed the egregious error you point out. Updates have already gone into F-12 and F-13, and should be part of the next F-11 compose. I will now write "I will not generate pretty graphs with doxygen" one thousand times.
Thanks, Jerry. I am sure all mirror admins will appreciate that. Doxygen should problably learn to produce svg, if it doesn't already, so we could keep some pretty in.
cvc3-2.1-3.fc11 has been pushed to the Fedora 11 stable repository. If problems still persist, please make note of it in this bug report.