[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 #5 from David A. Wheeler <dwheeler at dwheeler.com>  2009-12-21 23:16:57 EDT ---
Jerry James said:
> 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....

Ooops, I wasn't clear enough.  Sorry.  I would like to see the capability of
patch0 eventually merged into upstream, so that builders could easily remove
the PVS-unique version of mona.  By "optional", I meant "see if you could get
SRI to add this option to PVS, enabling the removal of its local 'mona'
library, so that future builds will not require as much patching".

> I asked Sam for the missing documentation files at the beginning of November. 
He has never replied.

Okay.  Not a big deal.

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

Yes, there's no naming conflict of the *packages*.  But if you install pvs-sbcl
and lvm2, there are two files in two different executable directories with the
same name: /usr/bin/pvs and /sbin/pvs.  Is there a possibility that at any time
someone will call the "wrong" one?

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

I'll have to look.

I ran PVS on that system at one time, and it's possible that I didn't clean it
up properly.  I'll try again on a different system; if that works, then clearly
it was just a bad test on my part.

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

Thanks, that info helps.  24 hours wasn't enough in my case, so clearly there
is something very wrong.

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