[Bug 548607] Review Request: pvs-sbcl - SRI's Prototype Verification System
bugzilla at redhat.com
bugzilla at redhat.com
Fri Dec 18 14:59:44 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 #3 from David A. Wheeler <dwheeler at dwheeler.com> 2009-12-18 09:59:42 EDT ---
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)...
--
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.
More information about the Fedora-package-review
mailing list