Please do not reply directly to this email. All additional comments should be made in the comments box of this bug. https://bugzilla.redhat.com/show_bug.cgi?id=548607 --- Comment #19 from David A. Wheeler <dwheeler@xxxxxxxxxxxx> 2009-12-28 23:51:07 EDT --- While you worked on the 32-bit issue, I tried the package out on a 64-bit install. I tried 2.20091008svn.fc12 on Fedora 12 as x64_64 (64-bit), and PVS worked just fine. But I did have some questions/issues after doing it. First, my simple smoke tests look good. After building and installing, I used my trivial "mortability.pvs" file from <http://www.dwheeler.com/trusting-trust/mortality.pvs> and invoked the program as: pvs-sbcl mortality.pvs I left-clicked on the socrates_mortal claim, invoked "PVS/Prover Invocation/prove", and when the interactive prover area popped up, I typed in: (grind :rewrites ("all_men_mortal")) That proved it, so it printed "Q.E.D." and wrote the proof file "mortality.prf". Now for a few comments on the RPM packaging... I think it is CRITICALLY important that the rpm Description state something like this: Note that the main executable "pvs" has been renamed to "pvs-sbcl". *ALL* the docs say that to invoke pvs you type "pvs", but that would invoke /sbin/pvs on a Fedora system instead. That's a nasty gotcha, and since I don't think we can/should rename /sbin/pvs, I think clearly stating that up-front is necessary. A few more comments about the "Description" text. I think you should simply drop the last sentence of the RPM description (everybody improves programs as they learn stuff, nothing special here). The next-to-last sentence doesn't add much, but its mention of "formal methods" is probably useful (someone searching for "formal methods" would correctly find PVS). I would also add to the description something about SRI; that way, someone searching on "SRI" would find this too. I did an rpmlint, and got some warnings. Specifically, I did: rpmlint pvs-sbcl.spec `find .. -name 'pvs*.rpm'` and got these warnings: pvs-sbcl.x86_64: W: unstripped-binary-or-object /usr/lib64/pvs/bin/ix86_64-Linux/runtime/ws1s.so pvs-sbcl.x86_64: W: unstripped-binary-or-object /usr/lib64/pvs/bin/ix86_64-Linux/b64 pvs-sbcl.x86_64: W: unstripped-binary-or-object /usr/lib64/pvs/bin/ix86_64-Linux/runtime/mu.so pvs-sbcl.x86_64: W: executable-stack /usr/lib64/pvs/bin/ix86_64-Linux/runtime/pvs-sbclisp 2 packages and 1 specfiles checked; 0 errors, 4 warnings. These are all semi-unavoidable due to the Lisp implementation, correct? Good luck on figuring out the 32-bit issue! -- 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. _______________________________________________ Fedora-package-review mailing list Fedora-package-review@xxxxxxxxxx http://www.redhat.com/mailman/listinfo/fedora-package-review