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

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



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

_______________________________________________
Fedora-package-review mailing list
Fedora-package-review@xxxxxxxxxx
http://www.redhat.com/mailman/listinfo/fedora-package-review

[Index of Archives]     [Fedora Legacy]     [Fedora Desktop]     [Fedora SELinux]     [Yosemite News]     [KDE Users]     [Fedora Tools]