;;; Make sure the soundness bug related to *1* fns and :program mode is gone. 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 !>(certify-book "bk1") CERTIFICATION ATTEMPT FOR "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk1.lisp" ACL2 Version 3.6.1 * Step 1: Read "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk1.lisp" and compute its check sum. * Step 2: There were two forms in the file. We now attempt to establish that each form, whether local or non-local, is indeed an admissible embedded event form in the context of the previously admitted ones. ACL2 >>(DEFUN FOO (X) (DECLARE (XARGS :MODE :PROGRAM)) (CAR X)) Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO * Step 3: That completes the admissibility check. Each form read was an embedded event form and was admissible. We now retract back to the initial world and try to include the book. This may expose local incompatibilities. Summary Form: ( INCLUDE-BOOK "bk1" ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) * Step 4: Write the certificate for "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk1.lisp" in "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk1.cert" , and compile the expansion file, /v/filer4b/v41q001/moore/public_html/acl2/se\ minar/2010.05-12-kaufmann/hcomp-tests/bk1@expansion.lsp. * Step 5: Compiling the functions defined in "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk1.lisp". Writing book expansion file, /v/filer4b/v41q001/moore/public_html/acl2/seminar\ /2010.05-12-kaufmann/hcomp-tests/bk1@expansion.lsp. "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk1.lx64fsl" Note: Deleting book expansion file, /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/bk1@expansion.lsp. Summary Form: (CERTIFY-BOOK "bk1" ...) Rules: NIL Warnings: None Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04) "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk1.lisp" ACL2 !>(u) 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(certify-book "bk2") ; certified in 3.6.1/GCL; proof of BUG should fail cleanly CERTIFICATION ATTEMPT FOR "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk2.lisp" ACL2 Version 3.6.1 * Step 1: Read "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/bk2.lisp" and compute its check sum. * Step 2: There were six forms in the file. We now attempt to establish that each form, whether local or non-local, is indeed an admissible embedded event form in the context of the previously admitted ones. ACL2 >>(DEFUN FOO (X) (CAR X)) Since FOO is non-recursive, its admission is trivial. We could deduce no constraints on the type of FOO. Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 >>(DEFUN BAR (X) (FOO X)) Since BAR is non-recursive, its admission is trivial. We could deduce no constraints on the type of BAR. Summary Form: ( DEFUN BAR ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) BAR ACL2 >>(DEFTHM FACT (NULL (BAR 3)) :RULE-CLASSES NIL) But we reduce the conjecture to T, by the :executable-counterparts of BAR and NULL. Q.E.D. Summary Form: ( DEFTHM FACT ...) Rules: ((:EXECUTABLE-COUNTERPART BAR) (:EXECUTABLE-COUNTERPART NULL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >>(ENCAPSULATE NIL (LOCAL (INCLUDE-BOOK "bk1")) (DEFTHM BUG (NOT (NULL (BAR 3))) :RULE-CLASSES NIL)) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 >>(LOCAL (INCLUDE-BOOK "bk1")) Summary Form: ( INCLUDE-BOOK "bk1" ...) 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/bk1.lisp" ACL2 >>(DEFTHM BUG (NOT (NULL (BAR 3))) :RULE-CLASSES NIL) By the :executable-counterparts of BAR and NULL we reduce the conjecture to Goal' NIL. Summary Form: ( DEFTHM BUG ...) Rules: ((:EXECUTABLE-COUNTERPART BAR) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART NULL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) --- The key checkpoint goal, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal' NIL ACL2 Error in ( DEFTHM BUG ...): See :DOC failure. ******** FAILED ******** ACL2 Warning in ( ENCAPSULATE NIL (LOCAL ...) ...): The attempted ENCAPSULATE has failed while trying to establish the admissibility of one of the (local or non-local) forms in the body of the ENCAPSULATE. Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( ENCAPSULATE NIL (LOCAL ...) ...): See :DOC failure. ******** FAILED ******** ACL2 Warning in CERTIFY-BOOK: The attempted CERTIFY-BOOK has failed while trying to establish the admissibility of one of the (local or non-local) forms in the book to be certified. Summary Form: (CERTIFY-BOOK "bk2" ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) ACL2 Error in (CERTIFY-BOOK "bk2" ...): See :DOC failure. ******** FAILED ******** ACL2 !>