[Bug 456398] Review Request: why - Why software verification platform

[bugzilla at redhat.com]

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

Summary: Review Request: why - Why software verification platform


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





------- Additional Comments From dwheeler at dwheeler.com  2008-07-23 14:36 EST -------
Must-do's:
* You renamed "cpulimit" to "why-cpulimit", which is sensible enough, but at
least gwhy (and maybe others) still call "cpulimit", so the whole thing fails. 
Quick test:
 sudo yum install -y zenon
 rpmbuild -ba ~/rpmbuild/SPECS/why.spec
 sudo rpm -ivh ~/rpmbuild/RPMS/*/why*.rpm
 cd ~/rpmbuild/BUILD/why-2.13/examples-c/tutorial
 gwhy binary_search.c
 # then click on the "Zenon" column.  Nothing works. Doing:
 strace -f -e trace=process gwhy binary_search.c
 # Note that that it's trying to run "cpulimit" instead. Ooops.
 # After fixing that, re-test.
* Something else is wrong with the installation; even trivial tests of
  caduceus fail.  After building, doing:
  cd ~/rpmbuild/BUILD/why-2.13/examples-c/tutorial
  caduceus max.c
  make -f max.makefile zenon
 Ends in failure. Running:
    strace -v -f -e trace=process make -f max.makefile zenon
 shows that the makefile invokes dp, which in turn tries to call zenon.
 But trying to invoke zenon on the generated file:
   zenon zenon/max_why.znn
 fails with a syntax error.  (I guess it's possible it has a bad bug
 in Zenon.)
* I believe you're missing some "Requires:".  I could "yum erase tcl tk",
  and still install ALL the programs (including gwhy).  rpm can automatically
  deduce a lot of dependencies from library information, but it will miss
  stuff (e.g., stuff invoked via shell/command line).  I was expecting
  gwhy, at least, to have more dependencies.  I think that's a blocker.
* Shouldn't the why-summer-school.tar.gz line include the URL?
* Can you confirm that Fedora has the legal right to redistribute the included
documents?  Fedora doesn't require the right to modify them (though that'd be
nice), but we need to make sure that it's legal to redistributed them.  (Of
course, if we could redistribute the .tex source files, that'd be even better.)

Here are a few suggestions:
* No %check section.   You ought to have SOME test in there, at least as a
'smoke test' to make sure everything can run with a trivial input.  The build's
"bench" subdirectory has useful tests (though you can't run "./bench" directly -
looks like they've changed --type-only and didn't fix the tests).
* You ought to install the examples that come with the distribution, those in
the build directory's "examples/" and "examples-c".  I suggest copying them to
be placed somewhere under /usr/share/doc/..../examples. (you probably want it
further organized than that). The Caduceus web page (http://caduceus.lri.fr/)
points some out.  For the trick to doing this, see:
http://fedoraproject.org/wiki/PackageMaintainers/PackagingTricks#Examples
* /usr/bin/dp is an absurdly short name for /usr/bin, and almost certain to
conflict with SOMETHING.  You might consider renaming that, too.
* I'm slightly surprised that Caduceus, Krakatoa, and Jessie aren't split into
separate packages.  Did you consider splitting them up?  Debian seems to have
done the same thing, so I won't make that a blocker.
* Is there other documentation you can include, e.g., specifically for Caduceus,
Krakatoa, and Jessie?  I see that the makefile can generate the documents, but
that the release doesn't include the source .tex files.
* The description isn't very clear for the unwashed masses, and it should
clearly suggest installing zenon and Coq.  Also: I don't think "why" accepts ML,
really; it accepts the "why" language, which is ML-like but isn't ML.

Other comments:
* License is OSS (GPLv2).  I checked to see if it should be "GPLv2+",
  but the file COPYING makes it clear that this spec file is correct -
  it is GPLv2 alone, not GPLv2+.
* When starting up gwhy, shouldn't it only show the proof tools that are
installed as the default?  I guess that would be additional functionality,
though, so not required for initial packaging.
* In the longer term, the PVS support files should be added too.  But since
there's no Fedora PVS package, that's probably impractical to test.  If PVS is
added to Fedora, then adding those would be a good idea.

I'll try to do a full review later.


-- 
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, or are watching someone who is.