[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 #26 from David A. Wheeler <dwheeler at dwheeler.com>  2010-01-02 15:38:04 EDT ---
I've resolved most other questions, other than the library-file items above
(the 2 MUSTs), but I got a weird difference between the svn version and what
you sent.

First, though, the good news.  Koji (scratch) build with dist-f12 worked
correctly:
 $ koji build --scratch dist-f12 ./pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm 
...
1899006 build (dist-f12, pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm): open
(ppc04.phx2.fedoraproject.org) -> closed
  0 free  0 open  3 done  0 failed
1899006 build (dist-f12, pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm) completed
successfully
Also, silly me, the spec uses "ExclusiveArch" and I've tested both of them, so
obviously we're fine in terms of architectural support.


HOWEVER, when I downloaded the source code using the spec directions (including
svn), I found this incredibly tiny difference:
[dwheeler at eve SOURCES]$ diff -u -r pvs-4.2 ~/temp/pvs-4.2
diff -u -r pvs-4.2/lib/bitvectors/bv_mult_div_rem.pvs
/home/dwheeler/temp/pvs-4.2/lib/bitvectors/bv_mult_div_rem.pvs
--- pvs-4.2/lib/bitvectors/bv_mult_div_rem.pvs  2002-12-18 20:23:50.000000000
-0500
+++ /home/dwheeler/temp/pvs-4.2/lib/bitvectors/bv_mult_div_rem.pvs     
2002-12-18 20:23:50.000000000 -0500
@@ -9,7 +9,7 @@
 %
 %  Author: Bart Jacobs
 %  Started: Wednesday 24 May 00 10:59:26 bart at frustratie
-%  Last-modified: $Date: 2002-12-18 18:23:50 -0700 (Wed, 18 Dec 2002) $
+%  Last-modified: $Date: 2002-12-18 20:23:50 -0500 (Wed, 18 Dec 2002) $
 %  Last-modified by: $Author: owre $


I can't see how this change makes a *difference*, but it's still a difference.

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