;;; Tests that illustrate order of loads, as well as warnings and errors: Welcome to Clozure Common Lisp Version 1.5-dev-r13559M-trunk (LinuxX8664)! ACL2 Version 3.6.1 built May 12, 2010 07:09:02. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 3.6.1. Level 1. Cbd "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/". Distributed books directory "/v/filer4b/v11q001/acl2/devel/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(value :q) Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ? [RAW LISP] (setq *load-compiled-verbose* t) T ? [RAW LISP] (LP) ACL2 Version 3.6.1. Level 1. Cbd "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/". Distributed books directory "/v/filer4b/v11q001/acl2/devel/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(include-book "book1") Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book1.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book2a.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book3a.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book4.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book2b.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book3b.lx64fsl. Summary Form: ( INCLUDE-BOOK "book1" ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/book1.lisp" ACL2 !>(u) 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>^Z Suspended > rm book4.lx64fsl > fg acl2c 3 3 ACL2 !>(include-book "book1") Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book1.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book2a.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book3a.lx64fsl. ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "book4" ...): Unable to load compiled file for book /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book4.lisp because the compiled file does not exist. See :DOC include-book. Here is the sequence of books with loads of compiled or expansion files that have led down to the printing of this message, where the load for each is halted during the load for the next: /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book1.lisp /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book2a.lisp /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book3a.lisp Summary Form: ( INCLUDE-BOOK "book1" ...) Rules: NIL Warnings: Compiled file Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/book1.lisp" ACL2 !>(u) 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(include-book "book1" :load-compiled-file nil) Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book2a.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book3a.lx64fsl. ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "book4" ...): Unable to load compiled file for book /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book4.lisp because the compiled file does not exist. See :DOC include-book. Here is the sequence of books with loads of compiled or expansion files that have led down to the printing of this message, where the load for each is halted during the load for the next: /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book2a.lisp /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book3a.lisp Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book2b.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book3b.lx64fsl. Summary Form: ( INCLUDE-BOOK "book1" ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/book1.lisp" ACL2 !>(u) 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(include-book "book1" :load-compiled-file t) Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book1.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book2a.lx64fsl. Note: loading file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05- 12-kaufmann/hcomp-tests/book3a.lx64fsl. HARD ACL2 ERROR in ( INCLUDE-BOOK "book4" ...): Unable to load compiled file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book4.lisp because the compiled file does not exist. See :DOC include-book. This is an error because we are underneath an include-book for "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/book1.lisp" that specified :LOAD-COMPILE-FILE T; see :DOC include-book. Here is the sequence of books with loads of compiled or expansion files that have led down to the printing of this message, where the load for each is halted during the load for the next: /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book1.lisp /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book2a.lisp /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book3a.lisp ACL2 Error in TOP-LEVEL: Evaluation aborted. To debug see :DOC print- gv, see :DOC trace, and see :DOC wet. ACL2 !>(include-book "book4" :load-compiled-file t) HARD ACL2 ERROR in ( INCLUDE-BOOK "book4" ...): Unable to load compiled file /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/book4.lisp because the compiled file does not exist. See :DOC include-book. This is an error because an include-book for this book specified :LOAD- COMPILE-FILE T; see :DOC include-book. No load was in progress for any parent book. ACL2 Error in TOP-LEVEL: Evaluation aborted. To debug see :DOC print- gv, see :DOC trace, and see :DOC wet. ACL2 !>