[Bug 548607] Review Request: pvs-sbcl - SRI's Prototype Verification System

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


https://bugzilla.redhat.com/show_bug.cgi?id=548607





--- Comment #19 from David A. Wheeler <dwheeler at dwheeler.com>  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.