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