[Bug 456398] Review Request: why - Why software verification platform
bugzilla at redhat.com
bugzilla at redhat.com
Wed Jul 30 18:24:19 UTC 2008
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-30 14:24 EST -------
I have created a new version to address your comments. It is based off of
why-2.14, a new release which incorporates some of the issues I mentioned here
that I reported to upstream.
SRPM: http://www.duke.edu/~amd34/why/why-2.14-1.fc9.src.rpm
SPEC: http://www.duke.edu/~amd34/why/why.spec
(In reply to comment #2)
> 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.
dp, cpulimit were renamed to why-dp, why-cpulimit in 2.14. With gwhy I can
successfully prove swap0.mlw from the examples. (Note: other files may time
out... this is a very hit or miss thing. There are more issues on this note that
I have been discussing with upstream.)
> * 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.)
The Zenon syntax error (their file format changed and upstream was not aware) is
fixed in 2.14.
> * 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.)
I actually decided the user would be better off visiting the why manual page for
supplementary documentation besides the current manual - it's in a moderate
state of flux anyway. (As a result, I removed the summer school tar and informed
the user about the location of the website in README.why.)
> 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).
A test is now performed: why is run on a file and its output is compared to a
known result.
> * 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
Done. Appears in %{_defaultdocdir}/examples/(c or mlw)/<example name>
> * 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'm still putting these together for now.
> * 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.
Caduceus and Krakatoa manuals are now included.
> * 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.
Description was modified.
--
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.
More information about the Fedora-package-review
mailing list