Spec URL: http://www.dwheeler.com/minisat2.spec SRPM URL: http://www.dwheeler.com/minisat2-070721-3.fc9.src.rpm Description: MiniSat is a minimalistic, open-source Boolean satisfiability problem (SAT) solver, developed for researchers and developers alike. Winning all the industrial categories of the SAT 2005 competition, MiniSat is a good starting point both for future research in SAT, and for applications using SAT. A SAT solver can determine if it is possible to find assignments to boolean variables that would make a given expression true, if the expression is written with only AND, OR, NOT, parentheses, and boolean variables. If the expression is satisfiable, MiniSAT can also produce a set of assignments that make the expression true. Although the problem is NP-complete, SAT solvers (like this one) are often able to decide this problem in a reasonable time frame. ================================================ * CLean rpmlint (.spec/.rpm/.src.rpm) * Clean koji build for all f9 archs * Open source software license (MIT) * Meets all guidelines (to the best of my knowledge) They used to use x.y versioning, but now seem to emphasize dates; have posted a question about version numbering to the packaging list. The package is named "minisat2" in part because that is its name in Debian (consistency seemed like a good idea). The program doesn't come with any (useful) documentation, so I wrote documentation, which is posted on the web and included in the package. The program didn't come with any tests, so I created a simple "smoke test", which is included in %check.
This looks mostly good to me. It's unfortunate to see that some people seem to have forgotten what happened a little under nine years ago and have fallen back to using two-digit years, but that's not up to you. I think the package in Debian is named minisat2 because that's actually the name of the software according to upstream, and of course that's the best name to use. Please consistently use the macro-ized forms; either use things like "cp -p" or use "%{cp_p}" but don't use both. (You have two macro forms in %install.) Personally I don't see the point in the extra typing that comes with the macros, but it's your choice; you just need to be consistent. Please add comments on the upstream status of the included patches. http://fedoraproject.org/wiki/Packaging/PatchUpstreamStatus Nice touch providing documentation, although it would be good if that was sent upstream as well. It's interesting that a few source files aren't in the debuginfo package; it looks like they're just dead code (e.g. BasicHeap.h isn't referenced anywhere). * source files match upstream: ddc2ed421a538a349ddab58d3958076d73813925ff08361e6292583d3b87248e minisat2-070721.zip c02847f5dedcf757917a8dd321a8314d1d21268f54823e17ef392311d539afe1 minisat-user-guide-1.0.html * package meets naming and versioning guidelines. * specfile is properly named and is cleanly written. X specfile does not use macros consistently. * summary is OK. * description is OK. * dist tag is present. * build root is OK. * license field matches the actual license. * license is open source-compatible. * license text included in package. * latest version is being packaged. * BuildRequires are proper. * compiler flags are appropriate. * %clean is present. * package builds in mock (rawhide, x86_64). * package installs properly. * debuginfo package looks complete. * rpmlint is silent. * final provides and requires are sane: minisat2 = 070721-3.fc10 = libgcc_s.so.1()(64bit) libgcc_s.so.1(GCC_3.0)(64bit) libstdc++.so.6()(64bit) libstdc++.so.6(CXXABI_1.3)(64bit) libz.so.1()(64bit) * %check is present and all tests pass. * no shared libraries are added to the regular linker search paths. * owns the directories it creates. * doesn't own any directories it shouldn't. * no duplicates in %files. * file permissions are appropriate. * no scriptlets present. * code, not content. * documentation is small, so no -doc subpackage is necessary. * %docs are not necessary for the proper functioning of the package. * no headers. * no pkgconfig files. * no static libraries. * no libtool .la files.
Thanks SO MUCH for reviewing the package! I'll fix the "specfile does not use macros consistently" issue. (Thanks, I hadn't noticed that.) I'll just switch to normal commands and not macros for them. I'm not fond of upstream's version system either. If you're going to use a date, use YYYYMMDD! I'm thinking of changing the version field to "2.0" and placing the date in the release value instead (treating it as if it were an "interim" release): 0.1.YYYYMMDD or some such. That way, if they switch back to a more traditional version numbering system, no epoch will be needed. Sound reasonable? > Nice touch providing documentation, although it would be good if that was sent upstream as well. Thanks! I agree with getting the docs upstream, that was my plan anyway. (I'm treating the added documentation as a patch.) It's ridiculous to create a program with NO documentation of any kind, yet this sure isn't the only one :-(.
Ok, I'm back from vacation. Here's the revised spec/SRPM that addresses everything I know of: http://www.dwheeler.com/minisat2.spec http://www.dwheeler.com//minisat2-2.0-4.20070721.fc9.src.rpm This version: - Addresses comment 1 "Please consistently use the macro-ized forms" - Changes the version/release numbering convention to match Fedora NamingGuidelines even more precisely. - Documents when patches/documentation was sent upstream (I sent the documentation earlier; I've sent everything today via email to Niklas Sorensson. Niklas is interested in including the docs in an upcoming version.) rpmlint reports no errors or warnings on .spec, SRPM, and generated binary rpm. It builds for both dist-f9 and dist-f10 on all architectures (via koji).
I've talked with upstream; I think I've convinced them to switch to a sensible "2.1"-style version naming convention for their next release. If they do so, this package can be easily updated to match. Please review this new version, and let me know if it's approved. Thanks.
I've made a small tweak, and uploaded a new release: http://www.dwheeler.com/minisat2-2.0-5.20070721.fc9.src.rpm http://www.dwheeler.com/minisat2.spec This release adds use of the "-O3" optimization flag, to get more speed out of it. This program is often compiled with -O3, and speed is absolutely critical to it. I believe this package is ready: * All issues raised above have been resolved. * rpmlint 100% clean on spec, SRPM, and a binary RPM (i386/f9) * koji scratch build are 100% successful on dist-f8, dist-f9, and dist-f10. So, any additional comments or approval?
Unfortunately at the moment I'm on vacation up near the arctic circle in Norway and have only limited access to the Internet and hence my build systems. It's not realy possible to do package reviews with only web access but if I have a slack day when I can get my laptop in range of some wireless network then I'll try to finish this up.
FYI, my miniSAT2 documentation is also available on the web, here: http://www.dwheeler.com/essays/minisat-user-guide.html It's included in my package, because without at least some documentation on its input, there's no way to USE this tool. My documentation is released to the public domain (see the bottom), so there's no license issue. I've already offered up my documentation to the Debian packager of miniSAT, which unsurprisingly has lousy documentation. Thread here: http://groups.google.com/group/minisat/browse_thread/thread/4680c4579611d714 As I noted earlier, I've already sent the patches and the new documentation to upstream, and have hopes that upstream will eventually incorporate them. Note: Novell/SuSE has changed their package manager to use a SAT solver to speed up dependency analysis (to speed up installation). Presentation here: http://en.opensuse.org/Libzypp/Sat_Solver I do _not_ know which SAT solver SuSE uses; miniSAT is a possibility.
Hi - any chance you (or someone else) could look over this proposed package? This is now a blocker for this proposed Fedora 10 feature: https://fedoraproject.org/wiki/Features/Provers
I'm back in the country now (although badly jetlagged); I will try to get this finished up this evening.
Everything looks fine to me except the -O3 ricing. I have no specific problems with this if you have some results which actually indicate a performance improvement, but if you're just assuming that it must somehow be faster because the number is bigger then you really should just use the default flags. Can you provide some evidence that this makes a difference?
The -O3 option is the _normal_ optimization level for MiniSAT. If you look at their makefile, you'll see that upstream adds -O3 when THEY do a release version ("make release"). So, I'm really just being consistent with upstream, and I think that's a reasonable reason. I could develop some test suites to do timing tests, but is that necessary if it's just being consistent with upstream?
Just a quick note that the SAT resolver used by SUSE for their new package management system - zypper is available for review at https://bugzilla.redhat.com/show_bug.cgi?id=442714
I went and got some numbers, and -O3 is a waste of time. I'll need to tell upstream that. I created a test sample, and got these: With -O3: real 0m35.714s real 0m35.714s real 0m35.834s With -O2: real 0m35.296s real 0m35.301s So -O3 will be dumped.
Okay, new miniSAT2 uploaded: http://www.dwheeler.com/minisat2.spec http://www.dwheeler.com/minisat2-2.0-6.20070721.fc9.src.rpm This one leaves -O2, as it was. I left in the (tricky) lines that switch optimization level, in case it actually helps in a future version of gcc.
I should add that my -O2 vs. -O3 numbers were for 32-bit i386. Your mileage may vary. Indeed, it almost CERTAINLY will vary :-). 2-CPU, where for each: vendor_id : GenuineIntel cpu family : 15 model : 6 model name : Intel(R) Pentium(R) D CPU 3.60GHz stepping : 4 cpu MHz : 3591.136 cache size : 2048 KB ... bogomips : 7187.56
Thanks for doing that. We rarely see any measurable improvement with -O3 so it's always viewed with some skepticism. That doesn't mean that you can't turn it on in the future if you find that it actually makes a difference, but in that case you should docuemnt the performance issues in the specfile and be prepared to re-evaluate as the compiler evolves. Anyway, things look good to me now; sorry that my vacation slowed things down. APPROVED
New Package CVS Request ======================= Package Name: minisat2 Short Description: A minimalistic, open-source SAT solver Owners: dwheeler Branches: F-8 F-9 InitialCC: tibbs Cvsextras Commits: yes
Please do not include me in the InitialCC for this package. I review far too many packages to be CC'd on all of them. Also, one comment I might add is that there's no need to play any games with "newoptflags" because you're not changing anything. You might as well just remove, or at least comment out, that portion of the spec.
cvs done.
minisat2-2.0-7.20070721.fc9 has been submitted as an update for Fedora 9. /updates/minisat2-2.0-7.20070721.fc9
minisat2-2.0-7.20070721.fc9 has been pushed to the Fedora 9 stable repository. If problems still persist, please make note of it in this bug report.