Bug 555161 - Review Request: csisat - Tool for LA+EUF Interpolation
Review Request: csisat - Tool for LA+EUF Interpolation
Status: CLOSED ERRATA
Product: Fedora
Classification: Fedora
Component: Package Review (Show other bugs)
rawhide
All Linux
medium Severity medium
: ---
: ---
Assigned To: David A. Wheeler
Fedora Extras Quality Assurance
:
Depends On: 555160
Blocks: 555162
  Show dependency treegraph
 
Reported: 2010-01-13 15:37 EST by Jerry James
Modified: 2010-01-22 17:38 EST (History)
3 users (show)

See Also:
Fixed In Version: 1.2-2.fc12
Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of:
Environment:
Last Closed: 2010-01-22 17:32:01 EST
Type: ---
Regression: ---
Mount Type: ---
Documentation: ---
CRM:
Verified Versions:
Category: ---
oVirt Team: ---
RHEL 7.3 requirements from Atomic Host:
dwheeler: fedora‑review+
tibbs: fedora‑cvs+


Attachments (Terms of Use)

  None (edit)
Description Jerry James 2010-01-13 15:37:55 EST
Spec URL: http://jjames.fedorapeople.org/csisat/csisat.spec
SRPM URL: http://jjames.fedorapeople.org/csisat/csisat-1.2-1.fc12.src.rpm
Description:
CSIsat is an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols.  This implementation combines the efficiency of linear programming for solving the arithmetic part with the efficiency of a SAT solver to reason about the boolean structure.
Comment 1 David A. Wheeler 2010-01-17 21:43:30 EST
I've started looking over the .spec file, here are some initial comments...

# FIXME: %%{?_smp_mflags} doesn't work
 Should the "FIXME" really be there?  I'd just state that "smp_mflags"
 doesn't work, and move on; smp_mflags doesn't work for LOTS of package builds.

# Make sure we don't use the bundled version of picosat
rm -fr picosat-632
 I suggest changing "picosat-632" to "picosat-*"; that way,
 updates to the package are less likely to unintentionally re-include this.

# Get rid of inappropriate executable bits
chmod a-x L* R* T*
 This is mysterious to readers, and could easily go wrong on future versions.
 I strongly recommend changing this to:
chmod a-x *.txt
 which fixes the same files, but for a far more obvious reason :-).

The one-line summary "Tool for LA+EUF Interpolation" is incomprehensible
for the uninitiated; can we make that clearer?
I'll have to admit that I can't think of an easy way to make the short
one clearer.

The multi-line description needs to be clearer and note the acronyms. I.E.,
"of rational linear arithmetic (LA) and equality with uninterpreted function
(EUF) symbols...." (since the acronyms are used in the summary).
And frankly, a less-forbidding description would be good.
What's an "interpolator"?  What does this do, WITHOUT using specialized terms?
E.G.,
 This reads a set of mathematical formulas that may combine variables,
addition, multiplication, comparisons (<,>, etc.), as well as boolean
expressions (and, or, not).  It determines if it is possible to set the
variables to values so that the set of formulas are all simultaneously
true (if it can, then the set of formulas is "satisfiable").

Unfortunately, since "picosat-devel" isn't in the Fedora repository, I can't easily use a koji build to test this :-(.

The ReadMe.txt file says that "The PicoSAT integration is experimental"; I presume that the default csi_dpll is proprietary, correct?  If that's right, then I guess this is what we need to do.

I used rpmlint, and got no warnings or errors (good!):
  rpmlint csisat.spec ../RPMS/i586/csisat-* ../SRPMS/csisat-1.2-1.fc11.src.rpm 
 3 packages and 1 specfiles checked; 0 errors, 0 warnings.
Comment 2 David A. Wheeler 2010-01-17 21:57:39 EST
I did a simple "smoke test" and csisat worked. I ran it with: csisat
and fed it the following input:
 a > 0 ;
 a < 4
It reported as output:
 Satisfiable: and [ (0 < a), (a < 4)]

(I.E., it's possible to set "a" so that it's >0 and < 4.)
Comment 3 David A. Wheeler 2010-01-17 22:16:49 EST
Here's my review.  I didn't find any additional issues, so please respond to my notes in comment 1.  I normally use mock/koji to test "did you get all the BuildRequires and architectures", and this package's dependency on picosat-devel makes that non-trivial (because that's not in the Fedora repository).  Is there any reason to believe that the buildrequires set is complete, and/or that all the architectures not excluded are okay?  (I don't want to go down a rat-hole on those if that's already been addressed.)


#  MUST: rpmlint must be run on every package. The output should be posted in the review.[1]

OK.  See 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 .

Generally okay, but see my notes in comment 1.

# MUST: The package must be licensed with a Fedora approved license and meet the Licensing Guidelines .
OK.  Apache Software License 2.0, listed as ASL 2.0, okay per http://fedoraproject.org/wiki/Licensing#Good_Licenses

# MUST: The License field in the package spec file must match the actual license. [3]

OK.  License.txt specifically says this.  I also sampled two files in the source directory, csisatAst.ml and csisatUtils.ml, and they agreed.

# 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
 wget http://csisat.googlecode.com/files/csisat-1.2.zip
 md5sum csisat-1.2.zip ~/rpmbuild/SOURCES/csisat-1.2.zip 
 fa0fec35362b452ba564f0f82086295f  csisat-1.2.zip
 fa0fec35362b452ba564f0f82086295f  /home/dwheeler/rpmbuild/SOURCES/csisat-1.2.zip

# MUST: The package MUST successfully compile and build into binary rpms on at least one primary architecture. [7]
OK.  Used 32-bit x86.

# 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 as best I can tell.
It excludes those where ocaml is not available:
ExcludeArch:    sparc64 s390 s390x
I usually test this with koji, but this package depends on another package that's not in the Fedora repository, so I can't easily do that.

# 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 as best I can tell.
I usually test this with koji, but this package depends on another package that's not in the Fedora repository, so I can't easily do that.

# 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]

NA

# 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 (I used rpmls, looks fine).

# 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.  Uses $RPM_BUILD_ROOT format (vs. %buildroot).

# 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]

NA.  What is this "lots of documentation" problem :-) ?

# 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]

NA

# 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

# 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]

NA

# MUST: In the vast majority of cases, devel packages must require the base package using a fully versioned dependency: Requires: %{name} = %{version}-%{release} [23]

NA

# 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


Again, see comment 1.
Comment 4 David A. Wheeler 2010-01-18 12:31:50 EST
I did an additional test of the BuildRequires info, and all seems fine.  I did a mock build, specially installing picosat into it, and it built.

Mock can rebuild packages when some dependencies aren't in a repository, unsurprisingly.  Unfortunately, the instructions on how to use mock to do this were terrible.  So I fixed up this Wiki page to explain to future packagers how to do this:
https://fedoraproject.org/wiki/Using_Mock_to_test_package_builds
Comment 5 Jerry James 2010-01-19 15:47:21 EST
I leave FIXMEs for myself when I find a package that won't build in parallel out of the box.  I can generally fix those if I try hard enough.  This one was just missing dependency information for the OCaml sources, easily generated with ocamldep.  With that in place, I get good parallel builds.  (I have an 8-core box, so I can crank the parallelism way up to try to trigger problems.)

I took your suggestions on altering the %prep section of the spec file.

I agree that the summary is totally opaque to the uninitiated.  On the other hand, the uninitiated also won't have any idea what to do with this package, so I'm not sure this is really a problem.  That's really just an excuse; I have no idea how to make it clearer.

I took your suggestion on the longer description, although note that I sneakily kept my original version, too. :-)

The default csi_dpll is actually written in OCaml, and is part of this package.  You have the choice of using it, or the external picosat library.  The picosat integration may well be experimental, but since the package tries to build it by default, I thought I had better provide it.

New URLs:

Spec URL: http://jjames.fedorapeople.org/csisat/csisat.spec
SRPM URL: http://jjames.fedorapeople.org/csisat/csisat-1.2-2.fc12.src.rpm
Comment 6 David A. Wheeler 2010-01-19 16:09:29 EST
I can't rebuild this version.

I suspect that the parallelism isn't really working, and the resulting race conditions cause build failures.  Doing this on an x86_64, Fedora 12.  When I do "rpmbuild -ba csisat.spec", it fails; here are 3 attempts:

... TRY #1:
ocamlc.opt -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c src/csisatAst.ml
mv  src/csisatUtils.o  obj/csisatUtils.o
mv  src/csisatAst.cmx obj/csisatAst.cmx
mv  src/csisatAst.cmi  obj/csisatAst.cmi
make[1]: Leaving directory `/home/dwheeler/rpmbuild/BUILD/csisat-1.2/server'
ocamlyacc src/io/csisatInfixParse.mly 
mv  src/csisatAst.cmo  obj/csisatAst.cmo
mv  src/io/csisatInfixParse.ml obj/csisatInfixParse.ml
mv  src/csisatAst.o  obj/csisatAst.o
mv  src/io/csisatInfixParse.mli  obj/csisatInfixParse.mli
ocamllex.opt -o obj/csisatInfixLex.ml src/io/csisatInfixLex.mll 
40 states, 1373 transitions, table size 5732 bytes
ocamlopt.opt -inline 10 -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c obj/csisatInfixParse.ml
File "obj/csisatInfixParse.ml", line 1, characters 0-1:
Error: Could not find the .cmi file for interface obj/csisatInfixParse.mli.
make: *** [obj/csisatInfixParse.cmx] Error 2
error: Bad exit status from /var/tmp/rpm-tmp.IbC1EW (%build)



... TRY #2:
ocamlc.opt -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c src/csisatUtils.ml
make[1]: Leaving directory `/home/dwheeler/rpmbuild/BUILD/csisat-1.2/server'
mv  src/csisatOrdSet.cmo  obj/csisatOrdSet.cmo
mv  src/csisatUtils.cmx obj/csisatUtils.cmx
mv  src/csisatUtils.cmi  obj/csisatUtils.cmi
mv  src/csisatOrdSet.o  obj/csisatOrdSet.o
mv  src/csisatUtils.cmo  obj/csisatUtils.cmo
mv  src/csisatUtils.o  obj/csisatUtils.o
ocamlopt.opt -inline 10 -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c src/csisatAst.ml
ocamlyacc src/io/csisatInfixParse.mly 
mv  src/io/csisatInfixParse.ml obj/csisatInfixParse.ml
mv  src/io/csisatInfixParse.mli  obj/csisatInfixParse.mli
ocamllex.opt -o obj/csisatInfixLex.ml src/io/csisatInfixLex.mll 
ocamlopt.opt -inline 10 -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c obj/csisatInfixParse.ml
40 states, 1373 transitions, table size 5732 bytes
ocamlc.opt -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c src/csisatAst.ml
File "src/io/csisatInfixParse.mly", line 20, characters 15-24:
Error: Unbound module CsisatAst
make: *** [obj/csisatInfixParse.cmx] Error 2
make: *** Waiting for unfinished jobs....
mv  src/csisatAst.cmx obj/csisatAst.cmx
mv  src/csisatAst.cmi  obj/csisatAst.cmi
mv  src/csisatAst.cmo  obj/csisatAst.cmo
mv  src/csisatAst.o  obj/csisatAst.o
make: *** wait: No child processes.  Stop.
error: Bad exit status from /var/tmp/rpm-tmp.vZFA74 (%build)

RPM build errors:



... TRY #3:
ocamlc.opt -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c src/csisatUtils.ml
mv  src/csisatUtils.cmx obj/csisatUtils.cmx
mv  src/csisatUtils.cmi  obj/csisatUtils.cmi
mv  src/csisatUtils.cmo  obj/csisatUtils.cmo
mv  src/csisatUtils.o  obj/csisatUtils.o
ocamlyacc src/io/csisatInfixParse.mly 
mv  src/io/csisatInfixParse.ml obj/csisatInfixParse.ml
mv  src/io/csisatInfixParse.mli  obj/csisatInfixParse.mli
ocamlc.opt -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c src/csisatAst.ml
make[1]: Leaving directory `/home/dwheeler/rpmbuild/BUILD/csisat-1.2/server'
ocamllex.opt -o obj/csisatInfixLex.ml src/io/csisatInfixLex.mll 
40 states, 1373 transitions, table size 5732 bytes
ocamlopt.opt -inline 10 -I obj -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/glpk_ml_wrapper/include -I /home/dwheeler/rpmbuild/BUILD/csisat-1.2/pico_ml_wrapper/include -c obj/csisatInfixParse.ml
mv  src/csisatAst.cmx obj/csisatAst.cmx
File "src/io/csisatInfixParse.mly", line 20, characters 15-24:
Error: Unbound module CsisatAst
mv  src/csisatAst.cmi  obj/csisatAst.cmi
make: *** [obj/csisatInfixParse.cmx] Error 2
make: *** Waiting for unfinished jobs....
mv  src/csisatAst.cmo  obj/csisatAst.cmo
mv  src/csisatAst.o  obj/csisatAst.o
error: Bad exit status from /var/tmp/rpm-tmp.C9VyuG (%build)


RPM build errors:
    Bad exit status from /var/tmp/rpm-tmp.C9VyuG (%build)
Comment 7 David A. Wheeler 2010-01-19 16:11:42 EST
BTW, I confirmed the parallel-build problem.

When I modified the .spec file to:
...
%build
make CFLAGS="$RPM_OPT_FLAGS -I%{_libdir}/ocaml -I%{_includedir}/glpk"
...

It built without problems.
Comment 8 Jerry James 2010-01-19 16:27:34 EST
This isn't a large enough package to worry obsessively about parallel make working, but I'd like to make one more try if you don't mind.  The problems you had were because the generated parser files weren't found by ocamldep.  The lexers have the necessary dependencies listed in the Makefile already, so I added the parser dependencies by hand.  I wonder why I didn't hit the problem you did?  Anyway, I believe all the dependencies are there now.  Would you mind trying again?  The URLs are the same as in comment 5.
Comment 9 David A. Wheeler 2010-01-19 17:05:42 EST
Everything looks good now!

It looks like you addressed all the comments above.

The parallel build works now.   I rebuilt three times, to try to trigger race conditions, and I saw no evidence of problems.

It seems to run fine.  I tried it both using the built-in SAT solver, and using the picoSAT SAT solver. To test it out, I used two test situations.
Test #1: Satisfiable
 a > 0 ;
 a < 4
Test #2: Unsatisfiable
a > 0 ; 
a < 0

I used -sat in all cases, and for both test situations I ran two test cases (pico and non-pico).... I used "-SATsolver pico" for pico.
They all produced the correct results.

rpmlint for this updated package is clean:
 rpmlint csisat.spec ../RPMS/x86_64/csisat-* ../SRPMS/csisat-1.2-2.fc12.src.rpm 
3 packages and 1 specfiles checked; 0 errors, 0 warnings.


APPROVED.
Comment 10 Jerry James 2010-01-19 17:37:23 EST
Thanks again, David.  I'll have to wait to build this one until the picosat update has gone through, but I'll get the CVS done.

New Package CVS Request
=======================
Package Name: csisat
Short Description: Tool for LA+EUF interpolation
Owners: jjames
Branches: F-11 F-12
InitialCC:
Comment 11 Jason Tibbitts 2010-01-19 20:01:05 EST
CVS done (by process-cvs-requests.py).
Comment 12 Fedora Update System 2010-01-21 14:45:55 EST
csisat-1.2-2.fc12 has been submitted as an update for Fedora 12.
http://admin.fedoraproject.org/updates/csisat-1.2-2.fc12
Comment 13 Fedora Update System 2010-01-21 14:46:01 EST
csisat-1.2-2.fc11 has been submitted as an update for Fedora 11.
http://admin.fedoraproject.org/updates/csisat-1.2-2.fc11
Comment 14 Fedora Update System 2010-01-22 17:31:56 EST
csisat-1.2-2.fc11 has been pushed to the Fedora 11 stable repository.  If problems still persist, please make note of it in this bug report.
Comment 15 Fedora Update System 2010-01-22 17:38:01 EST
csisat-1.2-2.fc12 has been pushed to the Fedora 12 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.