[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 amdunn at gmail.com  2008-07-24 16:11 EST -------
(In reply to comment #2)

I'm addressing these as I write, but I thought it'd be good to comment on how 
they're going/what I think about them.

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

Whoops, that's definitely my fault. Fixed in the next version (another patch).

> * 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 figured out that Why's Zenon output is wrong (it changed
between Zenon versions and remained undetected due to the
complete lack of Zenon documentation). I contacted upstream, and
they wrote a patch for me this morning. The change will be added
to the next version of Why.

> * 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.

I'll look at this.

> * Shouldn't the why-summer-school.tar.gz line include the URL?

No, because I created that file (a few PDFs packaged up).

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

I'll ask upstream.

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

Right, I originally wanted to run their tests, but they didn't
work. I did make my own (exceptionally brief) test, but I haven't
included it yet - I will.

> * 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

The example Makefiles are odd: the library files need to have
already been installed in the right places before the examples
can be compiled. Thus I can't put both in the build section, and
it doesn't seem right to put this in the install section...

> * /usr/bin/dp is an absurdly short name for /usr/bin, and almost certain to
> conflict with SOMETHING.  You might consider renaming that, too.

Changing dp's name would require patches for the following files:

Makefile.in
examples/Makefile.common
bench/java/bench

but I believe that's it (however, I could be introducing errors
here... again, maybe I'll suggest this change to upstream instead
who would better know how to fix it)

> * 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.

I wasn't quite sure, and Debian didn't, so I didn't.

> * 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.

I'll check on that.

> * 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.

True - I'll clarify that.

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