Bug 548607 - Review Request: pvs-sbcl - SRI's Prototype Verification System
Review Request: pvs-sbcl - SRI's Prototype Verification System
Status: CLOSED ERRATA
Product: Fedora
Classification: Fedora
Component: Package Review (Show other bugs)
rawhide
All Linux
medium Severity medium
: ---
: ---
Assigned To: David A. Wheeler
Fedora Extras Quality Assurance
:
Depends On:
Blocks:
  Show dependency treegraph
 
Reported: 2009-12-17 17:04 EST by Jerry James
Modified: 2010-01-07 16:56 EST (History)
5 users (show)

See Also:
Fixed In Version: 4.2-2.20100104svn.fc11
Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of:
Environment:
Last Closed: 2010-01-07 16:46:10 EST
Type: ---
Regression: ---
Mount Type: ---
Documentation: ---
CRM:
Verified Versions:
Category: ---
oVirt Team: ---
RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: ---
dwheeler: fedora‑review+
kevin: fedora‑cvs+


Attachments (Terms of Use)

  None (edit)
Description Jerry James 2009-12-17 17:04:34 EST
Spec URL: http://jjames.fedorapeople.org/pvs/pvs-sbcl.spec
SRPM URL: http://jjames.fedorapeople.org/pvs/pvs-sbcl-4.2-1.svn20091008.fc12.src.rpm
Description: 
PVS is a verification system: that is, a specification language integrated
with support tools and a theorem prover.  It is intended to capture the
state-of-the-art in mechanized formal methods and to be sufficiently rugged
that it can be used for significant applications.  PVS is a research
prototype: it evolves and improves as we develop or apply new capabilities,
and as the stress of real use exposes new requirements.

This is a build with SBCL.  The name was chosen so that builds with other Common Lisp engines in the future are not precluded.
Comment 1 David A. Wheeler 2009-12-17 18:39:58 EST
Thanks for doing this!  I did a quick scan of the spec file to start with, and have a few questions based on just that scan:
* I think the release number should be changed.  It's currently "1.svn20091008%{?dist}", but I don't think that will sort correctly with later items.  As I interpret "https://fedoraproject.org/wiki/Packaging:NamingGuidelines#PreReleasePackages", it should be something like "1.20091008svn%{?dist}".  I understand why you had to pull from svn, and agree with that decision, but I'm not sure that will sort well later.
* In the Summary, I'd add "(PVS)" at the end, to simply the job of keyword searchers.  The expanded name of PVS is more historical than reality... I think it's always referred to by its initials, not its full name.
* Patch0: I think it's okay for now, but in the long term, it might be nice for there to be a build option that skips mona and uses the existing packaging system.  That way it'll be easier to package for other distros, *and* it may reduce your longer-term pain as PVS changes.  I'd at least send the patch to the developers, explaining why it's needed.

I'm surprised at the number of "cannot be built" documents due to missing components; did you ask SRI for them?  At the least, I suspect Rushby wouldn't mind releasing his "/homes/rushby/tex/prelude" as OSS, or at least enough to build one of the docs.  I don't see a license issue with the spec the way it is, so I don't think that should hold up anything, but it'd be nice for the future.

I fear the amount of time it took to create *this* spec.  This is definitely not a program that was designed to be packaged.  Eek.
Comment 2 David A. Wheeler 2009-12-18 09:48:57 EST
A few additional random thoughts on this package:
* On Fedora there's already an /sbin/pvs (provided by lvm2), and /sbin is now in many users'  paths.  Is this likely to cause trouble?
* I see a "Provides:", that's good.  Should it provide "prototype-verification-system" instead of "pvs", since "pvs" has other meanings?
* It seems to me that PVS should have a desktop entry, as defined by http://standards.freedesktop.org/desktop-entry-spec/latest/
  That way, people can invoke it from the GUI, and double-click on ".pvs" files to invoke things correctly.  Something like this in pvs.desktop:
[Desktop Entry]
Version=1.0
Type=Application
Name=Prototype Verification System (PVS)
Comment=A verification system (a specification language integrated with support tools and a theorem prover).
TryExec=pvs
Exec=pvs %F
#  Icon=fooview
MimeType=image/x-pvs;

(Obviously, such a desktop entry should be submitted upstream, so that in the long term everyone will package it up & they'll maintain the desktop entry.)
Comment 3 David A. Wheeler 2009-12-18 09:59:42 EST
Is a *really* *really* long build time expected?

I've had it build overnight using "rpmbuild -ba pvs.spec".  It's STILL not done, after 14+ hours, and it's still burning cycles. I'm building on dual-processor Intel(R) Pentium(R) D CPU 3.60GHz (32-bit x86), 4GiB RAM, Fedora 11, 4GiB RAM. Also, I noticed some problems related to BDDs (see below).

"top" reports:
  PID USER      PR  NI  VIRT  RES  SHR S %CPU %MEM    TIME+  COMMAND            
14490 dwheeler  20   0  558m  44m  14m R 98.6  1.5 327758:45 sbcl               
22306 dwheeler  20   0 25984 9768 4576 R 97.6  0.3 879:42.54 emacs              
...

Here's the tail of the build output at this time:

=========================================================
Typechecking QuotientDistributive
QuotientDistributive typechecked: 9 TCCs, 0 proved, 0 subsumed, 9 unproved
Typechecking QuotientIteration
QuotientIteration typechecked: 7 TCCs, 0 proved, 0 subsumed, 7 unproved
Typechecking PartialFunctionDefinitions
PartialFunctionDefinitions typechecked: 1 TCC, 0 proved, 0 subsumed, 1 unproved
Typechecking PartialFunctionComposition
PartialFunctionComposition typechecked: 2 TCCs, 0 proved, 0 subsumed, 2 unproved
Done typechecking the prelude

;     (LIST SB-RUNTIME::UNP-FUNCTION SB-RUNTIME:*UNPARSE-STYLE*
;           SB-RUNTIME:*NO-ESCAPES* SB-RUNTIME:*SB-PRINT-DEPTH*
;           SB-RUNTIME:*SB-PRINT-LENGTH* SB-RUNTIME::*FORMATTING-OFF*)
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME:*FORMATTING-OFF*

;     (EVERY #'FBOUNDP PVS::*UNTYPECHECK-HOOK*)
; --> LET BLOCK 
; ==>
;   (MAP NIL
;        (LAMBDA (#:G2)
;          (LET ((SB-IMPL::PRED-VALUE #))
;            (UNLESS SB-IMPL::PRED-VALUE (RETURN-FROM #:BLOCK3 NIL))))
;        PVS::*UNTYPECHECK-HOOK*)
; 
; caught WARNING:
;   undefined variable: PVS::*UNTYPECHECK-HOOK*

;     (SB-RUNTIME:AW-TERM SB-RUNTIME::AW)
; 
; caught STYLE-WARNING:
;   undefined function: SB-RUNTIME:AW-TERM

;     (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::BP :VALUE
;      :UNITED-FLAG :CRS :SPACES :FORMAT)
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME::BP

;     (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::PLACE STREAM SB-RUNTIME::PLACE
;      SB-RUNTIME::LINETEXT SB-RUNTIME::LINENUMBER SB-RUNTIME::CHARNUMBER)
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME::CHARNUMBER

;     (ERGO-DISKSAVE TOOLS::ESS-FILENAME :RESTART-FUNCTION
;      #'(LAMBDA ()
;          (FORMAT T "~%~72:@<Welcome to the Ergo Support System~>~%")
;          (FORMAT T "~% Version ~A ~A" *ESS-VERSION* *ESS-VERSION-DATE*)
;          (FORMAT T "~% with ~A" TOOLS::ESS-STRING)
;          (FORMAT T "~% in ~A" TOOLS::BUILD-PARMS)
;          (FORMAT T "~% generated ~A by ~A~%~%" TOOLS::BUILD-TIME TOOLS::BUILDER)
;          (SETQ TOOLS::IN-REBORN-IMAGE-P T)
;          (CASE (WINDOWSYSTEM) (:X11 (UNLESS # # #)) (:X10 (WHEN # # #)))))
; 
; caught STYLE-WARNING:
;   undefined function: ERGO-DISKSAVE

;     (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::PLACE STREAM SB-RUNTIME::PLACE
;      SB-RUNTIME::LINETEXT SB-RUNTIME::LINENUMBER SB-RUNTIME::CHARNUMBER)
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME::LINENUMBER
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME::LINETEXT
; 
; caught STYLE-WARNING:
;   undefined function: SB-RUNTIME::PRINT-STRUCT

;     (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::TOKEN :KIND
;      :SUBKIND :VALUE :STR-VALUE)
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME:TOKEN
; 
; compilation unit finished
;   Undefined functions:
;     SB-RUNTIME:AW-TERM ERGO-DISKSAVE SB-RUNTIME::PRINT-STRUCT
;   Undefined variables:
;     SB-RUNTIME:*FORMATTING-OFF* PVS::*UNTYPECHECK-HOOK* SB-RUNTIME::BP SB-RUNTIME::CHARNUMBER SB-RUNTIME::LINENUMBER SB-RUNTIME::LINETEXT SB-RUNTIME:TOKEN
;   caught 8 WARNING conditions
;   caught 8 STYLE-WARNING conditions
[undoing binding stack and other enclosing state... done]
[saving current Lisp image into bin/ix86-Linux/runtime/pvs-sbclisp:
writing 3432 bytes from the read-only space at 0x01000000
writing 2256 bytes from the static space at 0x01100000
writing 92459008 bytes from the dynamic space at 0x09000000
done]
rm /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*
rm: cannot remove `/home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*': No such file or directory
make: [bin/ix86-Linux/runtime/pvs-sbclisp] Error 1 (ignored)
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/sbcl bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/mu.so bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/bdd-sbcl.lisp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/mu-sbcl.lisp bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/ix86-Linux/ws1s.so bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/utils/ix86-Linux/b64 bin/ix86-Linux
./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el \
                        -f set-prelude-files-and-regions
Loading /usr/share/emacs/site-lisp/site-start.d/focus-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/php-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/po-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/rpm-spec-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/rpmdev-init.el (source)...
Comment 4 Jerry James 2009-12-21 15:10:11 EST
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
Comment 5 David A. Wheeler 2009-12-21 23:16:57 EST
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.
Comment 6 David A. Wheeler 2009-12-21 23:48:31 EST
I found a bug in the build.  If you have a freshly-install sbcl, there hasn't been time for 'prelink' to mangle the sbcl executable.  The current script assumes that prelink *has* modified sbcl, and crashes when that's not so.  Here's the tail of the "rpmbuild -ba" output:

checking for emacs version >= 19... found 23.1.1
checking for etags... etags
checking for mkdir... mkdir
checking for tar... tar
checking for GNU tar version >= 1.11... found 1.22
checking for rm... rm
configure: creating ./config.status
config.status: creating Makefile
config.status: creating pvs
config.status: creating pvsio
config.status: creating doc/api/Makefile
config.status: creating doc/user-guide/Makefile
config.status: creating doc/language/Makefile
config.status: creating doc/language/pvs-doc.el
config.status: creating doc/prover/Makefile
+ cp -p /usr/bin/sbcl .
+ prelink -u ./sbcl
prelink: ./sbcl does not have .gnu.prelink_undo section
error: Bad exit status from /var/tmp/rpm-tmp.5D7Okc (%build)
Comment 7 David A. Wheeler 2009-12-22 08:14:31 EST
I changed the "prelink" line to:
   prelink -u ./sbcl || true
and re-ran "rpmbuild -ba pvs-sbcl.spec".  Again, after more than 12 hours it's stuck.
I did a "set | grep PVS" ; this system doesn't have *any* environment variables with "PVS" in the name.  So that can't be the problem.
Again, it's a 32-bit system.  I suspect that this build doesn't work on 32-bit systems.  Don't know why.

=================================

;     (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::TOKEN :KIND
;      :SUBKIND :VALUE :STR-VALUE)
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME:TOKEN
; 
; compilation unit finished
;   Undefined functions:
;     SB-RUNTIME:AW-TERM ERGO-DISKSAVE SB-RUNTIME::PRINT-STRUCT
;   Undefined variables:
;     SB-RUNTIME:*FORMATTING-OFF* PVS::*UNTYPECHECK-HOOK* SB-RUNTIME::BP SB-RUNTIME::CHARNUMBER SB-RUNTIME::LINENUMBER SB-RUNTIME::LINETEXT SB-RUNTIME:TOKEN
;   caught 8 WARNING conditions
;   caught 8 STYLE-WARNING conditions
[undoing binding stack and other enclosing state... done]
[saving current Lisp image into bin/ix86-Linux/runtime/pvs-sbclisp:
writing 3432 bytes from the read-only space at 0x01000000
writing 2256 bytes from the static space at 0x01100000
writing 92459008 bytes from the dynamic space at 0x09000000
done]
rm /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*
rm: cannot remove `/home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*': No such file or directory
make: [bin/ix86-Linux/runtime/pvs-sbclisp] Error 1 (ignored)
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/sbcl bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/mu.so bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/bdd-sbcl.lisp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/mu-sbcl.lisp bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/ix86-Linux/ws1s.so bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/utils/ix86-Linux/b64 bin/ix86-Linux
./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el \
                        -f set-prelude-files-and-regions
Loading /usr/share/emacs/site-lisp/site-start.d/focus-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/php-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/po-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/rpm-spec-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/rpmdev-init.el (source)...
Comment 8 Rex Dieter 2009-12-22 08:29:51 EST
mind you, the prelink hackery shouldn't be required in any mock/koji builds (only on live prelinked systems).
Comment 9 Jerry James 2009-12-22 12:44:12 EST
Comment 5: I did tell Sam Owre that I was doing this.  The comment in the spec file about not sending it upstream is therefore not completely accurate; I just don't expect upstream to apply it.  They are concentrated on providing a single download for researchers to grab, unpack, and get to work.  Finding dependencies would just complicate matters for them.

I renamed the binary from pvs to pvs-sbcl to avoid a name collision (see my response to comment 2 in comment 4).  So when I talked about the Provide, I was really only talking about the Provide, not the binary name.

The build hang has nothing to do with 32-bit vs. 64-bit systems, although I have never seen that hang with 64-bit Emacs (but have with 64-bit XEmacs).  The problem is that (X)Emacs is forking off a subprocess to run PVS, but isn't noticing when that process exits, and therefore waits forever.  Stephen Turnbull believes that this is a bug in X (see the URL in comment 4).  In any case, I believe I have found a workaround to the problem.  Briefly, I'm replacing (sit-for 1), which doesn't always notice changes in process status, with (accept-process-output nil 1), which does.

Comments 6 through 8: I have applied the "|| true" change to the spec file to avoid killing the build with an unprelinked sbcl binary.

New URLs:
http://jjames.fedorapeople.org/pvs/pvs-sbcl.spec
http://jjames.fedorapeople.org/pvs/pvs-sbcl-4.2-2.20091008svn.fc12.src.rpm
Comment 10 David A. Wheeler 2009-12-22 17:16:21 EST
Sadly, the workaround doesn't seem to work around.  It still hangs, same place, when trying to build PVS.  I fired up another build for "pvs-sbcl-4.2-2.20091008svn.fc12.src.rpm" (per comment 9 ), but it hangs the same spot.  I don't know why this happens, but I've put some details below in the hope that they help.

The rpmbuild hangs after printing this:

; caught STYLE-WARNING:
;   undefined function: SB-RUNTIME::PRINT-STRUCT

;     (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::TOKEN :KIND
;      :SUBKIND :VALUE :STR-VALUE)
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME:TOKEN
; 
; compilation unit finished
;   Undefined functions:
;     SB-RUNTIME:AW-TERM ERGO-DISKSAVE SB-RUNTIME::PRINT-STRUCT
;   Undefined variables:
;     SB-RUNTIME:*FORMATTING-OFF* PVS::*UNTYPECHECK-HOOK* SB-RUNTIME::BP SB-RUNTIME::CHARNUMBER SB-RUNTIME::LINENUMBER SB-RUNTIME::LINETEXT SB-RUNTIME:TOKEN
;   caught 8 WARNING conditions
;   caught 8 STYLE-WARNING conditions
[undoing binding stack and other enclosing state... done]
[saving current Lisp image into bin/ix86-Linux/runtime/pvs-sbclisp:
writing 3432 bytes from the read-only space at 0x01000000
writing 2256 bytes from the static space at 0x01100000
writing 92459008 bytes from the dynamic space at 0x09000000
done]
rm /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*
rm: cannot remove `/home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*': No such file or directory
make: [bin/ix86-Linux/runtime/pvs-sbclisp] Error 1 (ignored)
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/sbcl bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/mu.so bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/bdd-sbcl.lisp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/mu-sbcl.lisp bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/ix86-Linux/ws1s.so bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/utils/ix86-Linux/b64 bin/ix86-Linux
./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el \
                        -f set-prelude-files-and-regions
Loading /usr/share/emacs/site-lisp/site-start.d/focus-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/php-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/po-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/rpm-spec-mode-init.el (source)...
Loading /usr/share/emacs/site-lisp/site-start.d/rpmdev-init.el (source)...




{and there it sits.}

"top" shows that emacs is outrageously busy.  When I did the rpmbuild this time it's process 30005 that is busy busy busy; here are extracts from "ps -ef -H --width 99999":

dwheeler 29178 29115  0 15:33 pts/0    00:00:00           rpmbuild -ba pvs-sbcl.spec
dwheeler 29279 29178  0 15:33 pts/0    00:00:00             /bin/sh -e /var/tmp/rpm-tmp.ftYHYX
dwheeler 29829 29279  0 15:33 pts/0    00:00:00               make SBCLISP_HOME=/home/dwheeler/rpmbuild/BUILD/pvs-4.2 PVSPATH=/home/dwheeler/rpmbuild/BUILD/pvs-4.2/
dwheeler 29999 29829  0 16:25 pts/0    00:00:00                 /bin/sh ./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el -f set-prelude-files-and-regions
dwheeler 30005 29999 98 16:25 pts/0    00:29:32                   emacs -batch -load /home/dwheeler/rpmbuild/BUILD/pvs-4.2/emacs/go-pvs.el -l emacs/emacs-src/pvs-set-prelude-info.el -f set-prelude-files-and-regions
dwheeler 30006 30005  0 16:25 ?        00:00:00                     /home/dwheeler/rpmbuild/BUILD/pvs-4.2/bin/ix86-Linux/devel/pvs-sbclisp --noinform --no-userinit


The incessantly-busy 'emacs' process 30005 has fired off a "pvs-sbclisp" process.

I used gdb to try to get some backtrace information with 'gdb /usr/bin/emacs 30005'; gdb then told me to load the debug libraries by doing:
yum --enablerepo='*-debuginfo' install /usr/lib/debug/.build-id/80/ba91d6689ccf229be06e5e2d828cd9e95dc65b.debug
debuginfo-install alsa-lib-1.0.20-1.fc11.i586 atk-1.25.2-2.fc11.i586 bzip2-libs-1.0.5-5.fc11.i586 cairo-1.8.8-1.fc11.i586 dbus-libs-1.2.12-2.fc11.i586 e2fsprogs-libs-1.41.4-12.fc11.i586 expat-2.0.1-6.i586 fontconfig-2.7.1-1.fc11.i586 freetype-2.3.9-5.fc11.i586 giflib-4.1.6-2.fc11.i586 glib2-2.20.4-1.fc11.i586 glibc-2.10.1-4.i686 gtk2-2.16.5-1.fc11.i586 libICE-1.0.4-7.fc11.i586 libSM-1.1.0-4.fc11.i586 libX11-1.2.2-1.fc11.i586 libXau-1.0.4-5.fc11.i586 libXcomposite-0.4.0-7.fc11.i586 libXcursor-1.1.9-4.fc11.i586 libXdamage-1.1.1-6.fc11.i586 libXext-1.0.99.1-2.fc11.i586 libXfixes-4.0.3-5.fc11.i586 libXft-2.1.13-2.fc11.i586 libXi-1.2.1-1.fc11.i586 libXinerama-1.0.3-4.fc11.i586 libXpm-3.5.7-5.fc11.i586 libXrandr-1.2.99.4-3.fc11.i586 libXrender-0.9.4-5.fc11.i586 libattr-2.4.43-3.fc11.i586 libcap-2.16-4.fc11.1.i586 libcroco-0.6.2-2.fc11.i586 libgsf-1.14.11-3.fc11.i586 libjpeg-6b-45.fc11.i586 libotf-0.9.9-3.fc11.i586 libpng-1.2.37-1.fc11.i586 librsvg2-2.26.0-1.fc11.i586 libselinux-2.0.80-1.fc11.i586 libtiff-3.8.2-14.fc11.i586 libxcb-1.2-4.fc11.i586 libxml2-2.7.3-3.fc11.i586 m17n-lib-1.5.5-1.fc11.i586 ncurses-libs-5.7-2.20090207.fc11.i586 pango-1.24.5-1.fc11.i586 pixman-0.14.0-2.fc11.i586 zlib-1.2.3-22.fc11.i58

So I did that.   Here's the result of "list" command:
(gdb) list
5153          clear_input_pending ();
5154          QUIT;
5155        }
5156    
5157      return got_some_input;
5158    }
5159    ^L
5160    /* Given a list (FUNCTION ARGS...), apply FUNCTION to the ARGS.  */
5161    
5162    static Lisp_Object


and here's a backtrace, with local variable info:

(gdb) bt full
#0  0x081c1e64 in wait_reading_process_output (time_limit=-1, microsecs=0, 
    read_kbd=0, do_display=0, wait_for_cell=138051073, wait_proc=0x0, 
    just_wait_proc=0) at process.c:5158
        channel = 0
        nfds = 0
        Available = {fds_bits = {0 <repeats 32 times>}}
        Connecting = {fds_bits = {0 <repeats 32 times>}}
        check_connect = 0
        check_delay = 0
        no_avail = 0
        xerrno = 2
        proc = -1
        timeout = {tv_sec = 0, tv_usec = 0}
        end_time = {tv_sec = 1261522014, tv_usec = 51076}
        wait_channel = -1
        got_some_input = 0
#1  0x081c395b in Faccept_process_output (process=138051073, 
    seconds=138051073, millisec=0, just_this_one=138051073) at process.c:4211
        secs = 0
        usecs = 0
#2  0x08186ad6 in Feval (form=160954061) at eval.c:2386
        numargs = <value optimized out>
        argvals = {138051073, 138051073, 138051073, 138051073, 141037869, 
          137730968, 1, 1}
        args_left = 138051073
        i = 4
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138248977
        original_args = 138051073
        funcar = <value optimized out>
        backtrace = {next = 0xbfda33e0, function = 0xbfda3328, 
          args = 0xbfda32f0, nargs = 0, evalargs = 1 '\1', 
          debug_on_exit = 0 '\0'}
#3  0x08186d8d in Fprogn (args=160954069) at eval.c:450
        val = <value optimized out>
#4  0x08187720 in Fwhile (args=160954053) at eval.c:1112
        test = 160954021
        body = 160954069
#5  0x08186b77 in Feval (form=160954013) at eval.c:2323
        numargs = 0
        argvals = {-1076218560, -1076218920, -1076218924, -1, 0, 141024045, 1, 
          136506808}
        args_left = 160954053
---Type <return> to continue, or q <return> to quit---
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138192857
        original_args = 160954053
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3490, function = 0xbfda33f8, 
          args = 0xbfda33f4, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#6  0x08186d8d in Fprogn (args=161921117) at eval.c:450
        val = <value optimized out>
#7  0x08186b77 in Feval (form=161921141) at eval.c:2323
        numargs = 0
        argvals = {4, 3, 136506808, 1, 161543620, 161686483, 138051121, 
          -726506426}
        args_left = 161921133
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138190409
        original_args = 161921133
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3520, function = 0xbfda34a8, 
          args = 0xbfda34a4, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#8  0x08186997 in Feval (form=160953997) at eval.c:2434
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138389929
        original_args = 160954005
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3610, function = 0xbfda3538, 
          args = 0xbfda3534, nargs = -1, evalargs = 1 '\1', 
          debug_on_exit = 0 '\0'}
#9  0x08186d8d in Fprogn (args=160953989) at eval.c:450
        val = <value optimized out>
#10 0x08187acb in FletX (args=160953813) at eval.c:1034
        varlist = 138051073
        val = 161922733
        elt = 160953629
#11 0x08186b77 in Feval (form=160953557) at eval.c:2323
        numargs = 0
        argvals = {138051073, 160955317, -1076218232, 135818103, 160955101, 0, 
          2, 138051097}
---Type <return> to continue, or q <return> to quit---
        args_left = 160953813
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138192833
        original_args = 160953813
        funcar = <value optimized out>
        backtrace = {next = 0xbfda36c0, function = 0xbfda3628, 
          args = 0xbfda3624, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#12 0x08186d8d in Fprogn (args=160954133) at eval.c:450
        val = <value optimized out>
#13 0x08186b77 in Feval (form=160955293) at eval.c:2323
        numargs = 0
        argvals = {138051073, 1, -1076218168, 138051073, 160956933, 137730944, 
          2, 2}
        args_left = 160953541
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138190433
        original_args = 160953541
        funcar = <value optimized out>
        backtrace = {next = 0xbfda37e0, function = 0xbfda36d8, 
          args = 0xbfda36d4, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#14 0x08186d8d in Fprogn (args=160955253) at eval.c:450
        val = <value optimized out>
#15 0x08187918 in Flet (args=160955141) at eval.c:1090
        tem = 138051073
        elt = 138051073
        varlist = 138051073
#16 0x08186b77 in Feval (form=160955037) at eval.c:2323
        numargs = 0
        argvals = {-1076217776, -1076217896, -1076217900, -1, 0, 161922517, 
          138190409, -726506426}
        args_left = 160955141
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138192809
        original_args = 160955141
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3950, function = 0xbfda37f8, 
---Type <return> to continue, or q <return> to quit---
          args = 0xbfda37f4, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#17 0x08186d8d in Fprogn (args=160955005) at eval.c:450
        val = <value optimized out>
#18 0x08187009 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225
        val = <value optimized out>
        syms_left = 138051073
        next = 138364953
        i = 4
        optional = 1
        rest = 0
#19 0x0818711b in apply_lambda (fun=160954165, args=161127685, eval_flag=1)
    at eval.c:3156
        args_left = 138051073
        i = <value optimized out>
        tem = 138051073
#20 0x08186804 in Feval (form=161127653) at eval.c:2436
        fun = 0
        val = <value optimized out>
        original_fun = 160679793
        original_args = 161127685
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3a00, function = 0xbfda3968, 
          args = 0xbfda38a0, nargs = 4, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#21 0x08186d8d in Fprogn (args=161127757) at eval.c:450
        val = <value optimized out>
#22 0x08186b77 in Feval (form=161127597) at eval.c:2323
        numargs = 0
        argvals = {-1076217232, -1076217352, -1076217356, -1, 1073741824, 
          140924397, 138215665, 138051097}
        args_left = 161127605
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138190409
        original_args = 161127605
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3b20, function = 0xbfda3a18, 
          args = 0xbfda3a14, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#23 0x08186d8d in Fprogn (args=161127765) at eval.c:450
        val = <value optimized out>
---Type <return> to continue, or q <return> to quit---
#24 0x08187918 in Flet (args=161127589) at eval.c:1090
        tem = 138051121
        elt = 138051073
        varlist = 138051073
#25 0x08186b77 in Feval (form=161127557) at eval.c:2323
        numargs = 0
        argvals = {138051073, 138051073, -1076217048, 1, 138051073, 161686563, 
          -1076216952, 135819547}
        args_left = 161127589
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138192809
        original_args = 161127589
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3be0, function = 0xbfda3b38, 
          args = 0xbfda3b34, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#26 0x08186d20 in Fprog1 (args=161127773) at eval.c:481
        val = 138051073
        args_left = 161127773
#27 0x08186b77 in Feval (form=161127549) at eval.c:2323
        numargs = 0
        argvals = {138287577, 138051073, -1076216824, 161943842, 1, 1152, 
          -1076216840, 135784745}
        args_left = 161127773
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138192617
        original_args = 161127773
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3d00, function = 0xbfda3bf8, 
          args = 0xbfda3bf4, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#28 0x08186d8d in Fprogn (args=161127541) at eval.c:450

        val = <value optimized out>
#29 0x08187918 in Flet (args=161127477) at eval.c:1090
        tem = 138051073
        elt = 138051073
        varlist = 138051073
#30 0x08186b77 in Feval (form=161127461) at eval.c:2323
        numargs = 0
        argvals = {138237929, -1, -1076216524, 136506700, 4, 138486601, 
---Type <return> to continue, or q <return> to quit---
          -1076216552, 135749314}
        args_left = 161127477
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138192809
        original_args = 161127477
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3e70, function = 0xbfda3d18, 
          args = 0xbfda3d14, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#31 0x08186d8d in Fprogn (args=161127453) at eval.c:450
        val = <value optimized out>
#32 0x08187009 in funcall_lambda (fun=<value optimized out>, 

    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225
        val = <value optimized out>
        syms_left = 138051073
        next = 141206777
        i = 3
        optional = 1
        rest = 0
#33 0x0818711b in apply_lambda (fun=161127941, args=161090469, eval_flag=1)
    at eval.c:3156
        args_left = 138051073
        i = <value optimized out>
        tem = 138051073
#34 0x08186804 in Feval (form=161090461) at eval.c:2436
        fun = 0
        val = <value optimized out>
        original_fun = 160768913
        original_args = 161090469
        funcar = <value optimized out>
        backtrace = {next = 0xbfda3f40, function = 0xbfda3e88, 
          args = 0xbfda3dc0, nargs = 3, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#35 0x08187a1c in FletX (args=161090509) at eval.c:1028
        varlist = 161090501
        val = 138051073
        elt = 161090453
#36 0x08186b77 in Feval (form=161090349) at eval.c:2323
        numargs = 0
        argvals = {38, 161956788, 17591862, 137734976, -1076215960, 138051073, 
          -1076215976, 135813586}
        args_left = 161090509
---Type <return> to continue, or q <return> to quit---
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138192833
        original_args = 161090509
        funcar = <value optimized out>
        backtrace = {next = 0xbfda40b0, function = 0xbfda3f58, 
          args = 0xbfda3f54, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#37 0x08186d8d in Fprogn (args=161088661) at eval.c:450
        val = <value optimized out>
#38 0x08187009 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225
        val = <value optimized out>
        syms_left = 138051073
        next = 160768793
        i = 4
        optional = 1
        rest = 0
#39 0x0818711b in apply_lambda (fun=161088669, args=161371885, eval_flag=1)
    at eval.c:3156
        args_left = 138051073
        i = <value optimized out>
        tem = 160768961
#40 0x08186804 in Feval (form=161371853) at eval.c:2436

        fun = 0
        val = <value optimized out>
        original_fun = 160768841
        original_args = 161371885
        funcar = <value optimized out>
        backtrace = {next = 0xbfda41b0, function = 0xbfda40c8, 
          args = 0xbfda4000, nargs = 4, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#41 0x08187894 in Flet (args=161371949) at eval.c:1074
        tem = <value optimized out>
        elt = 161371845
        varlist = <value optimized out>
#42 0x08186b77 in Feval (form=161371837) at eval.c:2323
        numargs = 0
        argvals = {161686707, 138051073, -1076215352, 135658398, 137988592, 
          141330729, -1076215352, 135749314}
        args_left = 161371949
        i = <value optimized out>
        fun = <value optimized out>
---Type <return> to continue, or q <return> to quit---
        val = <value optimized out>
        original_fun = 138192809
        original_args = 161371949
        funcar = <value optimized out>
        backtrace = {next = 0xbfda4320, function = 0xbfda41c8, 
          args = 0xbfda41c4, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#43 0x08186d8d in Fprogn (args=161371725) at eval.c:450
        val = <value optimized out>
#44 0x08187009 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225
        val = <value optimized out>
        syms_left = 138051073
        next = 138344865
        i = 1
        optional = 0
        rest = 0
#45 0x0818711b in apply_lambda (fun=161372101, args=161655861, eval_flag=1)
    at eval.c:3156
        args_left = 138051073
        i = <value optimized out>
        tem = 138935811
#46 0x08186804 in Feval (form=161655853) at eval.c:2436
        fun = 0
        val = <value optimized out>
        original_fun = 161259201
        original_args = 161655861
        funcar = <value optimized out>
        backtrace = {next = 0xbfda44e0, function = 0xbfda4338, 
          args = 0xbfda4270, nargs = 1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#47 0x08187632 in internal_lisp_condition_case (var=138051073, 
    bodyform=161655853, handlers=161655893) at eval.c:1457
        val = <value optimized out>
        c = {tag = 138051073, val = 138051073, next = 0xbfda5614, gcpro = 0x0, 
          jmp = {{__jmpbuf = {161655888, 161655853, 161655845, -1076214696, 
                -1797473159, 280053014}, __mask_was_saved = 0, __saved_mask = {
                __val = {3218752592, 3218752440, 3218752256, 58657919, 0, 
                  138051073, 3218752472, 135749314, 138051073, 1, 3218752536, 
                  137734976, 3218752520, 138051073, 3218752616, 135817419, 
                  138051073, 3218752512, 138076932, 138076928, 138051073, 
                  161259632, 3218752584, 135750692, 161259633, 138051073, 
                  138051073, 138076928, 3218752736, 3218752552, 3218752496, 
                  161927669}}}}, backlist = 0xbfda44e0, 
---Type <return> to continue, or q <return> to quit---
          handlerlist = 0xbfda56dc, lisp_eval_depth = 12, pdlcount = 61, 
          poll_suppress_count = 1, 
interrupt_input_blocked = 0, 
          byte_stack = 0xbfda48f0}
        h = {handler = 161655893, var = 138051073, chosen_clause = 161655813, 
          tag = 0xbfda4374, next = 0xbfda56dc}
#48 0x081876db in Fcondition_case (args=161655845) at eval.c:1398
        bodyform = 161655853
        handlers = 0
        var = 138051073
#49 0x08186b77 in Feval (form=161655837) at eval.c:2323
        numargs = 0
        argvals = {161058099, 138051121, 138051121, 138051073, 138051073, 3, 
          -1076214520, 774}
        args_left = 161655845
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138192977
        original_args = 161655845
        funcar = <value optimized out>
        backtrace = {next = 0xbfda4590, function = 0xbfda44f8, 
          args = 0xbfda44f4, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#50 0x08186d8d in Fprogn (args=161658733) at eval.c:450
        val = <value optimized out>
#51 0x08186b77 in Feval (form=161658613) at eval.c:2323
        numargs = 0
        argvals = {0, 0, 0, -1076214276, 161661517, 1, 5, 3}
        args_left = 161658677
        i = <value optimized out>
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138190409
        original_args = 161658677
        funcar = <value optimized out>
        backtrace = {next = 0xbfda46f0, function = 0xbfda45a8, 
          args = 0xbfda45a4, nargs = -1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#52 0x08186d8d in Fprogn (args=161656701) at eval.c:450
        val = <value optimized out>
#53 0x08187009 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225
        val = <value optimized out>
        syms_left = 138051073
---Type <return> to continue, or q <return> to quit---
        next = 1
        i = 0
        optional = -1076214120
        rest = 135948681
#54 0x0818711b in apply_lambda (fun=161656773, args=138051073, eval_flag=1)
    at eval.c:3156
        args_left = 138051073
        i = <value optimized out>
        tem = 139764032
#55 0x08186804 in Feval (form=161656797) at eval.c:2436
        fun = 0
        val = <value optimized out>
        original_fun = 161251457
        original_args = 138051073
        funcar = <value optimized out>
        backtrace = {next = 0xbfda4838, function = 0xbfda4708, 
          args = 0xbfda4650, nargs = 0, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
#56 0x081a8581 in readevalloop (readcharfun=139764036, 
    stream=<value optimized out>, sourcename=<value optimized out>, 
    evalfun=0x8186600 <Feval>, printflag=0, unibyte=138051073, 
    readfun=138051073, start=<value optimized out>, end=138051073)
    at lread.c:1785
        c = <value optimized out>
        val = 0
        b = 0x854a140
        continue_reading_p = 1
        whole_buffer = 1
        first_sexp = <value optimized out>
#57 0x081a8830 in Feval_buffer (buffer=139764036, printflag=138051073, 
    filename=138971419, unibyte=138051073, do_allow_print=138051121)
    at lread.c:1846
        tem = <value optimized out>
        buf = 139764036
#58 0x0818507d in Ffuncall (nargs=6, args=0xbfda4880) at eval.c:3059
        fun = <value optimized out>
        original_fun = <value optimized out>
        funcar = <value optimized out>
        numargs = 5
        val = <value optimized out>
        backtrace = {next = 0xbfda49c8, function = 0xbfda4880, 
          args = 0xbfda4884, nargs = 5, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
        internal_args = 0xbfda4884
---Type <return> to continue, or q <return> to quit---
        i = 0
#59 0x081bae89 in Fbyte_code (bytestr=136555643, vector=136555660, maxdepth=48)
    at bytecode.c:678
        op = <value optimized out>
        stack = {pc = 0x83487a4 "\210,\16$\204\231", top = 0xbfda4894, 
          bottom = 0xbfda4880, byte_string = 136555643, 
          byte_string_start = 0x8348716 "\306\b!\204\22", 
          constants = 136555660, next = 0xbfda4da0}
        top = 0xbfda4880
        result = <value optimized out>
#60 0x08186f14 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232
        val = <value optimized out>
        syms_left = 138051073
        next = <value optimized out>
        i = 4
        optional = 1
        rest = 0
#61 0x08184edb in Ffuncall (nargs=5, args=0xbfda4a20) at eval.c:3102
        fun = 0
        original_fun = 138428073
        funcar = <value optimized out>
        numargs = 4
        val = <value optimized out>
        backtrace = {next = 0xbfda4ba0, function = 0xbfda4a20, 
          args = 0xbfda4a24, nargs = 4, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
        internal_args = <value optimized out>
        i = <value optimized out>
#62 0x08185279 in call4 (fn=138428073, arg1=138971419, arg2=138971419, 
    arg3=138051073, arg4=138051121) at eval.c:2899
        ret_ungc_val = 0
#63 0x081a972e in Fload (file=138967923, noerror=0, nomessage=138051121, 
    nosuffix=138051073, must_suffix=138051073) at lread.c:1208
        val = <value optimized out>
        stream = <value optimized out>
        fd = 3
        found = 138971419
        efound = <value optimized out>
        hist_file_name = 138971419
        newer = -1076213160
        compiled = 141274136
        handler = <value optimized out>
        safe_p = 141014557
---Type <return> to continue, or q <return> to quit---
        tmp = {141014221, 139155901}
        version = 0
#64 0x08186ab3 in Feval (form=141014261) at eval.c:2390
        numargs = <value optimized out>
        argvals = {138967923, 138051073, 138051121, 138051073, 138051073, 1, 
          -1076232192, 139787044}
        args_left = 138051073
        i = 5
        fun = <value optimized out>
        val = <value optimized out>
        original_fun = 138180161
        original_args = 141014253
        funcar = <value optimized out>
        backtrace = {next = 0xbfda4ce8, function = 0xbfda4bb8, 
          args = 0xbfda4b80, nargs = 4, evalargs = 1 '\1', 
          debug_on_exit = 0 '\0'}
#65 0x081a8581 in readevalloop (readcharfun=139787044, 
    stream=<value optimized out>, sourcename=<value optimized out>, 
    evalfun=0x8186600 <Feval>, printflag=0, unibyte=138051073, 
    readfun=138051073, start=<value optimized out>, end=138051073)
    at lread.c:1785
        c = <value optimized out>
        val = 0
        b = 0x854fb20
        continue_reading_p = 1
        whole_buffer = 1
        first_sexp = <value optimized out>
#66 0x081a8830 in Feval_buffer (buffer=139787044, printflag=138051073, 
    filename=138633667, unibyte=138051073, do_allow_print=138051121)
    at lread.c:1846
        tem = <value optimized out>
        buf = 139787044
#67 0x0818507d in Ffuncall (nargs=6, args=0xbfda4d30) at eval.c:3059
        fun = <value optimized out>
        original_fun = <value optimized out>
        funcar = <value optimized out>
        numargs = 5
        val = <value optimized out>
        backtrace = {next = 0xbfda4e78, function = 0xbfda4d30, 
          args = 0xbfda4d34, nargs = 5, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
        internal_args = 0xbfda4d34
        i = 0
#68 0x081bae89 in Fbyte_code (bytestr=136555643, vector=136555660, maxdepth=48)
---Type <return> to continue, or q <return> to quit---
    at bytecode.c:678
        op = <value optimized out>
        stack = {pc = 0x83487a4 "\210,\16$\204\231", top = 0xbfda4d44, 
          bottom = 0xbfda4d30, byte_string = 136555643, 
          byte_string_start = 0x8348716 "\306\b!\204\22", 
          constants = 136555660, next = 0xbfda5140}
        top = 0xbfda4d30
        result = <value optimized out>
#69 0x08186f14 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232
        val = <value optimized out>
        syms_left = 138051073
        next = <value optimized out>
        i = 4
        optional = 1
        rest = 0
#70 0x08184edb in Ffuncall (nargs=5, args=0xbfda4ed0) at eval.c:3102
        fun = 0
        original_fun = 138428073
        funcar = <value optimized out>
        numargs = 4
        val = <value optimized out>
        backtrace = {next = 0xbfda5078, function = 0xbfda4ed0, 
          args = 0xbfda4ed4, nargs = 4, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
        internal_args = <value optimized out>
        i = <value optimized out>
#71 0x08185279 in call4 (fn=138428073, arg1=138633667, arg2=138633667, 
    arg3=138051073, arg4=138051121) at eval.c:2899
        ret_ungc_val = 0
#72 0x081a972e in Fload (file=138614003, noerror=0, nomessage=138051121, 
    nosuffix=138051073, must_suffix=138051073) at lread.c:1208
        val = <value optimized out>
        stream = <value optimized out>
        fd = 3
        found = 138633667
        efound = <value optimized out>
        hist_file_name = 138633667
        newer = 0
        compiled = 141274136
        handler = <value optimized out>
        safe_p = 2003054437
        tmp = {141021573, 139155901}
        version = 0
---Type <return> to continue, or q <return> to quit---
#73 0x0818507d in Ffuncall (nargs=4, args=0xbfda50c0) at eval.c:3059
        fun = <value optimized out>
        original_fun = <value optimized out>
        funcar = <value optimized out>
        numargs = 3
        val = <value optimized out>
        backtrace = {next = 0xbfda5218, function = 0xbfda50c0, 
          args = 0xbfda50c4, nargs = 3, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
        internal_args = 0xbfda5020
        i = 0
#74 0x081bae89 in Fbyte_code (bytestr=136739427, vector=136739444, maxdepth=80)
    at bytecode.c:678
        op = <value optimized out>
        stack = {
          pc = 0x832d686 "\210*\202\276\3\16L띃#\2\347\16N\206\16\2\f\211A\24@!\36S\346\16S!\36T\352\16T\314ى$\210*\202\276\3\16L욃L\2\331\26Q\16N\206\67\2\f\211A\24@\211\26F;\204B\2\333\355!\210\356\347\16F!!\210\202\276\3\16LZ\2\360\331!\210\202\276\3\16L\361\232\203h\2\362\363!\210\202\276\3\321\364\16L\"\203y\2\365\16L!\26B\202\276\3\321\366\16L\"\203\226\2\365\325\326\16L\"!\26B\365\325\367\16L\"!\26A\202\276\3\332\16L\16H\"\211\26F\203\254\2\16FA@\f\233\24\202\276\3\332\16L\16J\"\211\26F\203\302\2\16FA@\f\233\24"..., top = 0xbfda50cc, 
          bottom = 0xbfda50c0, byte_string = 136739427, 
          byte_string_start = 0x832d48f "\306 \210\b\203\21", 
          constants = 136739444, next = 0xbfda52d0}
        top = 0xbfda50c0
        result = <value optimized out>
#75 0x08186f14 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232
        val = <value optimized out>
        syms_left = 138051073
        next = <value optimized out>
        i = 1
        optional = 0
        rest = 0
#76 0x08184edb in Ffuncall (nargs=2, args=0xbfda5260) at eval.c:3102
        fun = 0
        original_fun = 138988161
        funcar = <value optimized out>
        numargs = 1
        val = <value optimized out>
        backtrace = {next = 0xbfda53a8, function = 0xbfda5260, 
          args = 0xbfda5264, nargs = 1, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
---Type <return> to continue, or q <return> to quit---
        internal_args = <value optimized out>
        i = <value optimized out>
#77 0x081bae89 in Fbyte_code (bytestr=136725691, vector=136725708, maxdepth=56)
    at bytecode.c:678
        op = <value optimized out>
        stack = {
          pc = 0x832fdf0 "\210\16L\203\32\6\201", <incomplete sequence \334>, 
          top = 0xbfda5264, bottom = 0xbfda5260, byte_string = 136725691, 
          byte_string_start = 0x832f7e2 "\306 \20\307\21\n\23\310\311!\210\310\312!\210\310\313!\210\314\315!\211\34\307=\204;", constants = 136725708, 
          next = 0xbfda5460}
        top = 0xbfda5260
        result = <value optimized out>
#78 0x08186f14 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232
        val = <value optimized out>
        syms_left = 138051073
        next = <value optimized out>
        i = 0
        optional = 0
        rest = 0
#79 0x08184edb in Ffuncall (nargs=1, args=0xbfda53f0) at eval.c:3102
        fun = 0
        original_fun = 138870409
        funcar = <value optimized out>
        numargs = 0
        val = <value optimized out>
        backtrace = {next = 0xbfda55a0, function = 0xbfda53f0, 
          args = 0xbfda53f4, nargs = 0, evalargs = 0 '\0', 
          debug_on_exit = 0 '\0'}
        internal_args = <value optimized out>
        i = <value optimized out>
#80 0x081bae89 in Fbyte_code (bytestr=136722315, vector=136722332, maxdepth=48)
    at bytecode.c:678
        op = <value optimized out>
        stack = {
          pc = 0x833069a "\210+\340\341\342\"\210\343\321\344\"\211\36$;\203\254", top = 0xbfda53f0, bottom = 0xbfda53f0, byte_string = 136722315, 
          byte_string_start = 0x8330609 "\b\203\b", constants = 136722332, 
          next = 0x0}
        top = 0xbfda53f0
        result = <value optimized out>
#81 0x08186f14 in funcall_lambda (fun=<value optimized out>, 
    nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232
---Type <return> to continue, or q <return> to quit---
        val = <value optimized out>
        syms_left = 138051073
        next = <value optimized out>
        i = 0
        optional = -1076210292
        rest = 2682433
#82 0x0818711b in apply_lambda (fun=136722292, args=138051073, eval_flag=1)
    at eval.c:3156
        args_left = 138051073
        i = <value optimized out>
        tem = 138593888
#83 0x08186804 in Feval (form=138620021) at eval.c:2436
        fun = 0
        val = <value optimized out>
        original_fun = 138958121
        original_args = 138051073
        funcar = <value optimized out>
        backtrace = {next = 0x0, function = 0xbfda55b8, args = 0xbfda5500, 
          nargs = 0, evalargs = 0 '\0', debug_on_exit = 0 '\0'}
#84 0x0811d453 in top_level_2 () at keyboard.c:1368
No locals.
#85 0x08184491 in internal_condition_case (bfun=0x811d440 <top_level_2>, 
    handlers=138094225, hfun=0x8120850 <cmd_error>) at eval.c:1512
        val = 0
        c = {tag = 138051073, val = 138051073, next = 0xbfda5738, gcpro = 0x0, 
          jmp = {{__jmpbuf = {138593872, 138593872, 138593888, -1076209928, 
                -1795785607, 282255126}, __mask_was_saved = 0, __saved_mask = {
                __val = {27, 27, 3218757240, 135724656, 2774624, 0, 2775064, 
                  3218757360, 3218757288, 3218757300, 1, 1, 0, 134540224, 
                  3087905304, 0, 138377389, 138377389, 3218757320, 135444720, 
                  138377389, 0, 0, 0, 0, 0, 2817468, 3087925248, 3218757328, 
                  4294967295, 2772932, 134540224}}}}, backlist = 0x0, 
          handlerlist = 0x0, lisp_eval_depth = 0, pdlcount = 2, 
          poll_suppress_count = 1, interrupt_input_blocked = 0, 
          byte_stack = 0x0}
        h = {handler = 138094225, var = 138051073, chosen_clause = 134526964, 
          tag = 0xbfda5614, next = 0x0}
#86 0x08120605 in top_level_1 () at keyboard.c:1376
No locals.
#87 0x08184571 in internal_catch (tag=138090249, func=0x81205a0 <top_level_1>, 
    arg=138051073) at eval.c:1248
        c = {tag = 138090249, val = 138051073, next = 0x0, gcpro = 0x0, jmp = {
            {__jmpbuf = {138593872, 138593872, 138593888, -1076209656, 
                -1795933063, 282126102}, __mask_was_saved = 0, __saved_mask = {
---Type <return> to continue, or q <return> to quit---
                __val = {3218757620, 3218757768, 135396002, 3218757632, 0, 0, 
                  0, 3253566, 0, 0, 138076928, 138051073, 138291416, 
                  3218757608, 135750692, 138291417, 138288674, 138051073, 
                  138076928, 6, 110, 119, 4077456, 91, 110, 119, 138051097, 
                  58, 22, 0, 138291417, 138051073}}}}, backlist = 0x0, 
          handlerlist = 0x0, lisp_eval_depth = 0, pdlcount = 2, 
          poll_suppress_count = 1, interrupt_input_blocked = 0, 
          byte_stack = 0x0}
#88 0x08120681 in command_loop () at keyboard.c:1331
No locals.
#89 0x08120a4a in recursive_edit_1 () at keyboard.c:953
        val = <value optimized out>
#90 0x08120b72 in Frecursive_edit () at keyboard.c:1015
        buffer = 138051073
#91 0x08116ef2 in main (argc=0, argv=<value optimized out>) at emacs.c:1852
        dummy = -1076208744
        stack_bottom_variable = 8 '\b'
        do_initial_setlocale = 138593872
        skip_args = 1
        rlim = {rlim_cur = 10485760, rlim_max = 18446744073709551615}
        no_loadup = 0
        junk = 0x0
        dname_arg = 0x0



Sadness.  Any ideas?
Comment 11 Jerry James 2009-12-22 17:42:57 EST
That's annoying.  The workaround fixed the hang with 64-bit XEmacs, and 64-bit Emacs never seemed to have a problem.  So what's up with 32-bit Emacs?

I don't know, off the top of my head.  Can you try setting PVSEMACS=xemacs and see if you get the same hang?  If so, it really is a 32-bit versus 64-bit issue somehow, although I still fail to see how that could have anything to do with it.

If not, we'll just set PVSEMACS in the spec file to make sure we don't get a hung build for now, and I'll talk to the Emacs developers to see if they have any ideas.

Incidentally, there's another bug somewhere.  I was just working on a proof, tried to prove a TCC, and Lisp threw an error, claiming that *EXPRS-GENERATING-ACTUAL-TCCS* is unbound.  That isn't possible, since it is defvar'd in globals.lisp and given an initial value of nil.  I did a setq to nil, and was able to continue with the proof, but that shouldn't have happened...
Comment 12 David A. Wheeler 2009-12-22 19:19:17 EST
Okay, as you suggested I'm about to fire this off:
 export PVSEMACS=xemacs
 rpmbuild -ba pvs-sbcl.spec
I have to run an errand, but when I return, *hopefully* this will be done.

I don't know why *EXPRS-GENERATING-ACTUAL-TCCS* was unbound, but for all the world that looks like some sort of namespace issue (where the namespace used when reading globals.lisp isn't being used properly later).  There's actually a remarkable number of warnings when sbcl compiles PVS; the few that I looked at seemed to be just hints about how to generate faster code, and not real issues, but it's possible that at least one of those warnings is more serious.
Comment 13 David A. Wheeler 2009-12-22 23:14:16 EST
Drat, and double-drat.  Doing "export PVSEMACS=xemacs" has a useless effect... it merely means that xemacs gets stuck in an endless loop instead of emacs.

"top" reports that "xemacs" is very busy, essentially using the entire CPU:
31372 dwheeler  20   0 21724  12m 3552 R 97.3  2.5 164:51.99 xemacs
Note the "TIME" value of >164minutes.  Sure isn't 10 minutes.

Doing a ps -ef, I see:
dwheeler 30543 29115  0 19:56 pts/0    00:00:00 rpmbuild -ba pvs-sbcl.spec
dwheeler 30544 29115  0 19:56 pts/0    00:01:05 tee ,pvs-results
dwheeler 30645 30543  0 19:56 pts/0    00:00:00 /bin/sh -e /var/tmp/rpm-tmp.8WyTz0
dwheeler 31195 30645  0 19:57 pts/0    00:00:00 make SBCLISP_HOME=/home/dwheeler/rpmbuild/BUILD/pvs-4.2 PVSPATH=/home/dwheeler/rpmbuild/BUILD/pvs-4.2/
dwheeler 31366 31195  0 20:48 pts/0    00:00:00 /bin/sh ./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el -f set-prelude-files-and-regions
dwheeler 31372 31366 99 20:48 pts/0    02:43:13 xemacs -batch -load /home/dwheeler/rpmbuild/BUILD/pvs-4.2/emacs/go-pvs.el -l emacs/emacs-src/pvs-set-prelude-info.el -f set-prelude-files-and-regions
dwheeler 31374 31372  0 20:48 ?        00:00:00 /home/dwheeler/rpmbuild/BUILD/pvs-4.2/bin/ix86-Linux/devel/pvs-sbclisp --noinform --no-userinit

I don't actually *know* if this is a 32-bit vs. 64-bit issue, but IIRC you tested on 64-bit, while I'm testing on 32-bit, so it's an obvious difference in the test environment that *might* explain the difference in results.

This looks like exactly the same problem as before. There is an interesting oddity, though I don't know if it's important.  I though I might need to search through the build output later, so I ran the build through "tee" like this:
  rpmbuild -ba 2>&1 > ,pvs-results
Just like last time, it reported that it was loading "rpmdev-init.el" just before it got hung, but then it reported one additional line.  Its *last* line reported:
  Loading leim-list...
(*without* a terminating newline, oddly enough.)
So I got one extra line of output.  I'm not sure that is significant; that may be simply because I changed (slightly) how I invoked rpmbuild.  But maybe that's important.  Anyway, here's the tail of the build report:

; caught STYLE-WARNING:
;   undefined function: SB-RUNTIME::PRINT-STRUCT

;     (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::TOKEN :KIND
;      :SUBKIND :VALUE :STR-VALUE)
; 
; caught WARNING:
;   undefined variable: SB-RUNTIME:TOKEN
; 
; compilation unit finished
;   Undefined functions:
;     SB-RUNTIME:AW-TERM ERGO-DISKSAVE SB-RUNTIME::PRINT-STRUCT
;   Undefined variables:
;     SB-RUNTIME:*FORMATTING-OFF* PVS::*UNTYPECHECK-HOOK* SB-RUNTIME::BP SB-RUNTIME::CHARNUMBER SB-RUNTIME::LINENUMBER SB-RUNTIME::LINETEXT SB-RUNTIME:TOKEN
;   caught 8 WARNING conditions
;   caught 8 STYLE-WARNING conditions
[undoing binding stack and other enclosing state... done]
[saving current Lisp image into bin/ix86-Linux/runtime/pvs-sbclisp:
writing 3432 bytes from the read-only space at 0x01000000
writing 2256 bytes from the static space at 0x01100000
writing 92459008 bytes from the dynamic space at 0x09000000
done]
rm /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*
rm: cannot remove `/home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*': No such file or directory
make: [bin/ix86-Linux/runtime/pvs-sbclisp] Error 1 (ignored)
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/sbcl bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/mu.so bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/bdd-sbcl.lisp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/mu-sbcl.lisp bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/ix86-Linux/ws1s.so bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp bin/ix86-Linux/runtime/
cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/utils/ix86-Linux/b64 bin/ix86-Linux
./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el \
                        -f set-prelude-files-and-regions

  Loading /usr/share/xemacs/site-packages/lisp/site-start.d/rpmdev-init.el...
  Loading leim-list...




I have no idea why it's getting hung.
Comment 14 Jerry James 2009-12-23 00:33:47 EST
The hangs you are experiencing all appear to be happening in the same code where I initially experienced the hang.  If Stephen Turnbull is right, this is a bug in X, and if my attempted workaround doesn't do the job, then we're just sunk ... with an X build.  Let's try using emacs-nox or xemacs-nox.  I'll work up the necessary spec file changes tomorrow after a good night's rest.
Comment 15 David A. Wheeler 2009-12-23 10:37:11 EST
> Let's try using emacs-nox or xemacs-nox.

Agree.  That's an unfortunate solution if it's long-term, but it's a reasonable short-term solution *AND* it would definitely help narrow down where the bug is.

Please modify the spec so that it'll be easy to switch back to "normal" emacs or xemacs.  It's my hope that using *emacs-nox is a relatively temporary solution.

Your earlier patch modified "exit-pvs-process" by replacing (sit-for 1) with
(accept-process-output nil 1).  Although it's a nasty hack, you could instead repeatedly (1) wait for 1 second using sleep, then (2) use "system" to invoke "ps" directly and see if the process is gone.  Yeah, that's a nasty hack.  Might work, though.
Comment 16 Jerry James 2009-12-23 13:45:48 EST
Argh.  The elisp code calls add-submenu AT COMPILE TIME!  Since this function doesn't exist in (x)emacs-nox, the compilation fails.

I still don't understand why the accept-process-output hack isn't working for you, though.  It runs code that is supposed to check for process statuses, on both emacsen.  Since it solved the problem I was having with XEmacs, I know that code is being run.

I'm going to make a virtual 32-bit machine and see if I can debug the hang you're seeing.  It looks like the same hang, but may not be.
Comment 17 David A. Wheeler 2009-12-24 21:47:29 EST
I have no idea if this is related, but I found that
someone had to specially patch interaction between GIMP and emacs
when using emacs' sit-for.  Maybe this would help?:
http://github.com/pft/gimpmode/commit/296ca334d510975a5d271fb151e4250676f61ae3
Comment 18 David A. Wheeler 2009-12-24 22:24:42 EST
I've been hunting for other reports about problems with sit-for.  You may have seen all this, but perhaps I've found something you haven't seen.

Anyway, I found this PVS bug report:
  http://pvs.csl.sri.com/cgi-bin/pvs-bug?id=440
And maybe this is useful too:
  http://emacs-w3m.namazu.org/ml/msg09645.html

Good luck, and Merry Christmas!
Comment 19 David A. Wheeler 2009-12-28 23:51:07 EST
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!
Comment 20 Jerry James 2009-12-29 00:20:33 EST
Thanks for the comments.  I'll address those some time tomorrow.  I have figured out the problem with the 32-bit platform, and it is, in fact, a different hang than the one I was seeing on the 64-bit platform.  On the 32-bit platforms, Emacs is waiting for PVS forever, because the PVS process isn't exiting.  It looks like the immediate problem is that my patch to use the system Mona library isn't quite right.  I don't know why this didn't manifest on the 64-bit platform (maybe it would later on during the execution).

Anyway, I've got to figure out how to do this correctly now.  I'll try to do that tomorrow, too.
Comment 21 David A. Wheeler 2009-12-29 11:21:38 EST
Congrats for figuring out the 32-bit platform problem, that's great news!  Sounds like it needed fixing for 64-bit as well.

I can't wait for the next package revision!  Good luck.
Comment 22 Jerry James 2010-01-01 20:25:21 EST
Now that I'm done making merry, I had a chance to work on this again.  I found several more SBCL-specific changes that needed to be made to the PVS code base, so I've reworked the patches.  Give this a try:

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

This includes changes that were checked into PVS subversion over the last couple of weeks.
Comment 23 David A. Wheeler 2010-01-02 12:12:51 EST
Hooray!! This updated package now works on 32-bit (using Fedora 11).   It builds without hanging.  I also used the "mortality.pvs" demo, and PVS quickly proves "Socrates is mortal".  That's good, since Socrates has been dead a long time :-).  Anyway, that worked in 64-bit, now it works (again) in 32-bit.

I found no rpmlint warnings in this version (at least for the 32-bit version).  I did "rpmlint ./RPMS/i586/pvs-sbcl-4.2-2.20091229svn.fc11.i586.rpm ./SRPMS/pvs-sbcl-4.2-2.20091229svn.fc11.src.rpm ./SPECS/pvs-sbcl.spec" and it reported:
2 packages and 1 specfiles checked; 0 errors, 0 warnings.

I'll try 64-bit Fedora 12 next; presuming that works, I'll then walk through the package guideline checklist.
Comment 24 David A. Wheeler 2010-01-02 13:22:40 EST
This PVS also seems to work on 64-bit Fedora 12.  It builds fine. There are no rpmlint warnings or errors on this one, either:
 rpmlint pvs-sbcl.spec ../RPMS/x86_64/pvs-sbcl-4.2-2.20091229svn.fc12.x86_64.rpm ../SRPMS/pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm
 2 packages and 1 specfiles checked; 0 errors, 0 warnings.
Comment 25 David A. Wheeler 2010-01-02 14:43:43 EST
Okay, I reviewed the package using the guideline checklist at: https://fedoraproject.org/wiki/Packaging:ReviewGuidelines

I have questions/issues for two points:
    * MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. [10]
NO.  There are some files that are stored as shared library files:
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/
Granted, these probably aren't shared by other packages, but they MIGHT be.
    * MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1), then library files that end in .so (without suffix) must go in a -devel package. [20]
??? NOT SURE.  There are ".so" files not in a -devel package, but it's not clear that they SHOULD be in a -devel package.

Comments?  Perhaps I'm misunderstanding something?

There are a few things I need to do, too. I can't check the svn version at this instant (can't download), so I hope to do that soon.  I also intend to do a koji build, which will answer some.

Other than that, looks like we're off.  Here's the guideline checklist results:

    *  MUST: rpmlint must be run on every package. The output should be posted in the review.[1]

OK.  No warnings or errors.

    * MUST: The package must be named according to the Package Naming Guidelines.

OK.

    * MUST: The spec file name must match the base package %{name}, in the format %{name}.spec unless your package has an exemption. [2].

OK.

    * MUST: The package must meet the Packaging Guidelines.

OK.  At least, I don't see any violations.

    * MUST: The package must be licensed with a Fedora approved license and meet the Licensing Guidelines.

OK (GPLv2+).

    * MUST: The License field in the package spec file must match the actual license. [3]

OK.  It has the usual GPL LICENSE file.  The PVS website also specifically
states that it is GPL-licensed:
http://pvs.csl.sri.com/download.shtml

    * MUST: If (and only if) the source package includes the text of the license(s) in its own file, then that file, containing the text of the license(s) for the package must be included in %doc.[4]

OK.  See /usr/share/doc/pvs-sbcl-4.2/LICENSE

    * MUST: The spec file must be written in American English. [5]

OK.

    * MUST: The spec file for the package MUST be legible. [6]

OK.

    * MUST: The sources used to build the package must match the upstream source, as provided in the spec URL. Reviewers should use md5sum for this task. If no upstream URL can be specified for this package, please see the Source URL Guidelines for how to deal with this.

??? I need to check this later.  This package uses an SVN version, to pick up necessary patches.  The spec file documents that the extraction uses:
 svn export -r 5477 https://spartan.csl.sri.com/svn/public/pvs/trunk pvs-4.2
I'm having trouble downloading from SVN at this moment; I'll try again later.

    * MUST: The package MUST successfully compile and build into binary rpms on at least one primary architecture. [7]

OK.

    * MUST: If the package does not successfully compile, build or work on an architecture, then those architectures should be listed in the spec in ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in bugzilla, describing the reason that the package does not compile/build/work on that architecture. The bug number MUST be placed in a comment, next to the corresponding ExcludeArch line. [8]

OK to my knowledge.  I only tried x86, 32-bit and 64-bit.  Koji would answer this.

    * MUST: All build dependencies must be listed in BuildRequires, except for any that are listed in the exceptions section of the Packaging Guidelines ; inclusion of those as BuildRequires is optional. Apply common sense.

OK to my knowledge.  Koji would answer this.

    * MUST: The spec file MUST handle locales properly. This is done by using the %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.[9]

NA.  Only English.

    * MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. [10]

NO.  There are some files that are stored as shared library files:
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/
Granted, these probably aren't shared by other packages, but they MIGHT be.

    * MUST: Packages must NOT bundle copies of system libraries.[11]

OK.  There's a "/usr/lib64/pvs/wish", but this is a *directory* not wish itself.

    * MUST: If the package is designed to be relocatable, the packager must state this fact in the request for review, along with the rationalization for relocation of that specific package. Without this, use of Prefix: /usr is considered a blocker. [12]

NA.

    * MUST: A package must own all directories that it creates. If it does not create a directory that it uses, then it should require a package which does create that directory. [13]

OK.  I looked at %files, looks okay.

    * MUST: A Fedora package must not list a file more than once in the spec file's %files listings. [14]

OK.  Again, %files looks okay.

    * MUST: Permissions on files must be set properly. Executables should be set with executable permissions, for example. Every %files section must include a %defattr(...) line. [15]

The %files section has %defattr(); rpmls looks okay.

    * MUST: Each package must have a %clean section, which contains rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [16]

OK

    * MUST: Each package must consistently use macros. [17]

OK

    * MUST: The package must contain code, or permissable content. [18]

OK

    * MUST: Large documentation files must go in a -doc subpackage. (The definition of large is left up to the packager's best judgement, but is not restricted to size. Large can refer to either size or quantity). [19]

NA

    * MUST: If a package includes something as %doc, it must not affect the runtime of the application. To summarize: If it is in %doc, the program must run properly if it is not present. [19]

NA

    * MUST: Header files must be in a -devel package. [20]

NA

    * MUST: Static libraries must be in a -static package. [21]

NA

    * MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for directory ownership and usability). [22]

NA

    * MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1), then library files that end in .so (without suffix) must go in a -devel package. [20]

??? NOT SURE.  There are ".so" files not in a -devel package, but it's not clear that they SHOULD be in a -devel package.  Comments?


    * MUST: In the vast majority of cases, devel packages must require the base package using a fully versioned dependency: Requires: %{name} = %{version}-%{release} [23]

NA

    * MUST: Packages must NOT contain any .la libtool archives, these must be removed in the spec if they are built.[21]

NA

    * MUST: Packages containing GUI applications must include a %{name}.desktop file, and that file must be properly installed with desktop-file-install in the %install section. If you feel that your packaged GUI application does not need a .desktop file, you must put a comment in the spec file with your explanation. [24]

OK.  This was added recently as part of the packaging process.

    * MUST: Packages must not own files or directories already owned by other packages. The rule of thumb here is that the first package to be installed should own the files or directories that other packages may rely upon. This means, for example, that no package in Fedora should ever share ownership with any of the files or directories owned by the filesystem or man package. If you feel that you have a good reason to own a file or directory that another package owns, then please present that at package review time. [25]

OK.

    * MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [26]

OK.

    * MUST: All filenames in rpm packages must be valid UTF-8. [27]
OK.  ASCII.


    *  SHOULD: If the source package does not include license text(s) as a separate file from upstream, the packager SHOULD query upstream to include it. [28]

NA

    * SHOULD: The description and summary sections in the package spec file should contain translations for supported Non-English languages, if available. [29]

Don't, but not required.

    * SHOULD: The reviewer should test that the package builds in mock. [30]

I'll try to do this later.

    * SHOULD: The package should compile and build into binary rpms on all supported architectures. [31]

??? Partly done.  I used two.  Mock/koji should help determine for the others.

    * SHOULD: The reviewer should test that the package functions as described. A package should not segfault instead of running, for example.

OK. I did smoke tests for 32-bit and 64-bit.

    * SHOULD: If scriptlets are used, those scriptlets must be sane. This is vague, and left up to the reviewers judgement to determine sanity. [32]

NA.

    * SHOULD: Usually, subpackages other than devel should require the base package using a fully versioned dependency. [23]

NA

    * SHOULD: The placement of pkgconfig(.pc) files depends on their usecase, and this is usually for development purposes, so should be placed in a -devel pkg. A reasonable exception is that the main pkg itself is a devel tool not installed in a user runtime, e.g. gcc or gdb. [22]

NA

    * SHOULD: If the package has file dependencies outside of /etc, /bin, /sbin, /usr/bin, or /usr/sbin consider requiring the package which provides the file instead of the file itself. [33] 

NA
Comment 26 David A. Wheeler 2010-01-02 15:38:04 EST
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@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@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.
Comment 27 Jerry James 2010-01-02 19:32:15 EST
David, thanks for reviewing the package so thoroughly.  The packaging guidelines say, in section 1.24, "In addition, every binary RPM package which contains shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun."  This package does not put a shared library file in any of the dynamic linker's default paths, so this requirement is vacuously satisfied.

The .so files are covered by section 1.22.  Since the shared libraries are for PVS's use only, this section is also vacuously satisfied.

I can't account for the timestamp difference you see, but since the time is off by 2 hours in one direction and the time zone is off by 2 hours in the other direction, they represent the same time.  I live in the -0700 timezone.  I'm guessing you live in the -0500 timezone.
Comment 28 David A. Wheeler 2010-01-02 22:46:45 EST
> I can't account for the timestamp difference you see, but since the time is off
by 2 hours in one direction and the time zone is off by 2 hours in the other
direction, they represent the same time.

You're right!  They're the same time, and that text is the only "difference".  That is a weird thing that svn does, but that's a clear explanation... it appears that in certain cases, svn uses the local timezone when retrieving, and thus I see a "difference" that isn't really a difference at all.  Great; that means that that MUST is resolved.

And I see what you mean about the .so files.  You're right, those "MUST"s are vacuously satisfied.

So: all requirements are met.  Thank you SO MUCH for packaging PVS; this one required real work to make it 64-bit-ready, and was *tricky* for other reasons too.  Great job.

APPROVED.
Comment 29 Jerry James 2010-01-02 23:17:30 EST
New Package CVS Request
=======================
Package Name: pvs-sbcl
Short Description: Interactive theorem prover from SRI
Owners: jjames
Branches: F-11 F-12
InitialCC:
Comment 30 Alexander Kahl 2010-01-04 10:04:58 EST
Hi,

I've been following this review for some time now as I'm not aware of any existing self-executable CL-based packages in Fedora besides CL implementations themselves so this could well be the very first one; I would like to see things learned from the review in the wiki as I'm going to package CL stuff myself sometime in the future and I find the existing Lisp-related guidelines sparse; e.g. I'd conclude from what is written down right now that providing self-executable Lisp machines that are not the original implementations themselves is impossible, instead it looks like Lisp is treated like scripting languages in Fedora (which is - of course - utterly wrong) since the guidelines force use of cl- prefixes for both libs (OK) and programs (bad) and source code distribution only. I could be wrong here since the guidelines mentions "Libraries and Programs" in the headline but doesn't refer to the latter in the following body.

Source: http://fedoraproject.org/wiki/Packaging/Lisp#Guidelines_for_Libraries_and_Programs_written_in_Common_Lisp

Would you mind starting a discussion about this in fedora-devel? I'd really like to see this resolved in an official manner and make Lisp-based projects first-level citizens in Fedora.
Comment 31 David A. Wheeler 2010-01-04 10:43:27 EST
The second sentence of:
 http://fedoraproject.org/wiki/Packaging/Lisp#Guidelines_for_Libraries_and_Programs_written_in_Common_Lisp
is:
 "This document does not describe conventions and customs for application programs that are written in Common Lisp."
So that document doesn't apply.

To my knowledge, there are *no* special written guidelines for packaging applications *written* in Common Lisp (CL).  You just follow the usual conventions for packages (adding WHICH CL implementation you used in the package name).  I know that "maxima" is another packaged application written in CL, so PVS isn't unique.

It might be nice to have guidelines, but someone will have to figure out good guidelines first :-).
Comment 32 Alexander Kahl 2010-01-04 11:18:01 EST
Hi David,

(In reply to comment #31)
> The second sentence of:
> 
> http://fedoraproject.org/wiki/Packaging/Lisp#Guidelines_for_Libraries_and_Programs_written_in_Common_Lisp
> is:
>  "This document does not describe conventions and customs for application
> programs that are written in Common Lisp."
> So that document doesn't apply.
Ooh I must have missed that - thanks for pointing that out!

> To my knowledge, there are *no* special written guidelines for packaging
> applications *written* in Common Lisp (CL).  You just follow the usual
> conventions for packages (adding WHICH CL implementation you used in the
> package name).  I know that "maxima" is another packaged application written in
> CL, so PVS isn't unique.
Didn't know 'bout that one, thanks again.

> It might be nice to have guidelines, but someone will have to figure out good
> guidelines first :-).  
The original ones seem to have been written by Spot, I wonder if he just took over those from Debian or whether he really knows about coding Lisps.
Well the only "someones" in question is Fedorans who can code Lisp (or here CL in particular), right? So why not make something up?
Comment 33 Jerry James 2010-01-04 11:31:56 EST
I just started a thread to discuss the issues on fedora-devel, as requested.  Let's discuss the issues there, where others can see the discussion, instead of hidden away in this bug.
Comment 34 Kevin Fenzi 2010-01-04 15:09:42 EST
cvs done.
Comment 35 Fedora Update System 2010-01-04 18:21:37 EST
pvs-sbcl-4.2-2.20100104svn.fc12 has been submitted as an update for Fedora 12.
http://admin.fedoraproject.org/updates/pvs-sbcl-4.2-2.20100104svn.fc12
Comment 36 Fedora Update System 2010-01-04 18:21:42 EST
pvs-sbcl-4.2-2.20100104svn.fc11 has been submitted as an update for Fedora 11.
http://admin.fedoraproject.org/updates/pvs-sbcl-4.2-2.20100104svn.fc11
Comment 37 Alexander Kahl 2010-01-06 10:42:28 EST
David: I'd really appreciate if you'd also join the discussion Jerry started at fedora-devel :)
Comment 38 Fedora Update System 2010-01-07 16:46:03 EST
pvs-sbcl-4.2-2.20100104svn.fc12 has been pushed to the Fedora 12 stable repository.  If problems still persist, please make note of it in this bug report.
Comment 39 Fedora Update System 2010-01-07 16:56:35 EST
pvs-sbcl-4.2-2.20100104svn.fc11 has been pushed to the Fedora 11 stable repository.  If problems still persist, please make note of it in this bug report.

Note You need to log in before you can comment on or make changes to this bug.