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

Wed Dec 23 04:14:17 UTC 2009

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 #13 from David A. Wheeler <dwheeler at dwheeler.com>  2009-12-22 23:14:16 EDT ---
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.

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