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@xxxxxxxxx 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. _______________________________________________ Fedora-package-review mailing list Fedora-package-review@xxxxxxxxxx http://www.redhat.com/mailman/listinfo/fedora-package-review