[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 #4 from Jerry James <loganjerry at gmail.com>  2009-12-21 15:10:11 EDT ---
Thanks for all the comments, David.  Sorry to be slow responding.  Darn viruses
....

Comment 1: you're right about the version number.  I'll fix that.

There was a discussion on fedora-devel recently about not including the name of
the package in its Summary field, and rpmlint complains if you do that. 
However, you have a good point about the expansion of PVS being purely
historical.  I've changed the Summary to "Interactive theorem prover from SRI".

Patch0 is required for Fedora.  No bundled libraries are allowed without an
exception.  As far as I know, other distributions have similar rules, so I
don't see the point in making Patch0 optional.  Furthermore, the PVS copy of
mona has not kept up with upstream.  There are multiple bug fixes in the
current mona release that have never been copied over to the PVS version. 
(This is exactly the reason for the "no bundled libraries" rule, in fact.)  I
have, in fact, made Sam Owre aware that I'm doing this and why.

I asked Sam for the missing documentation files at the beginning of November. 
He has never replied.  I am not in contact with anyone else at SRI, but I
suppose I could try locating John Rushby's contact information.

Comment 2: I am also worried about that other "pvs".  I'll make this one
"pvs-sbcl".

I think the current Provides is okay.  /sbin/pvs is owned by the lvm2 package,
which only provides these:

config(lvm2) = 2.02.53-2.fc12
lvm2 = 2.02.53-2.fc12
lvm2(x86-64) = 2.02.53-2.fc12

so there is no conflict.  I did the "pvs" Provides so that libraries of PVS
theories can "Requires: pvs" and have that be satisfied by a PVS built by any
supported Common Lisp.

Thanks for the desktop entry.  I have added that, with some modifications
inspired by the coq desktop file.

Comment 3: Do you have PVSEMACS=xemacs in your environment?  If so, see
http://calypso.tux.org/pipermail/xemacs-beta/2009-December/018035.html

Those BDD-related messages are harmless.  They are due to the way the Makefiles
are set up, which assumes that you will be doing multiple builds in the same
directory.  You get those messages about failing to clean up the previous build
on the first build ... which, of course, is the ONLY build when constructing an
RPM.

The total build time for me is usually 7-8 minutes, by the way.

New files:
http://jjames.fedorapeople.org/pvs/pvs-sbcl.spec
http://jjames.fedorapeople.org/pvs/pvs-sbcl-4.2-1.20091008svn.fc12.src.rpm

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