;;; Potentially huge speed-up when there is heavy macroexpansion: > acl2c 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 !>(time$ (certify-book "speed-test1")) ; has taken almost 7s in CCL (5.2s in 3.6.1) CERTIFICATION ATTEMPT FOR "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test1.lisp" ACL2 Version 3.6.1 * Step 1: Read "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test1.lisp" and compute its check sum. * Step 2: There were four 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-FN (N) (DECLARE (XARGS :GUARD (NATP N))) (IF (ZP N) 1 (1- (+ (FOO-FN (1- N)) (FOO-FN (1- N)))))) The admission of FOO-FN is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). We observe that the type of FOO-FN is described by the theorem (INTEGERP (FOO-FN N)). We used primitive type reasoning. Computing the guard conjecture for FOO-FN.... The guard conjecture for FOO-FN is trivial to prove, given the :compound- recognizer rules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription rule FOO-FN. FOO-FN is compliant with Common Lisp. Summary Form: ( DEFUN FOO-FN ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION FOO-FN)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO-FN ACL2 >>(DEFMACRO FOO (N) (FOO-FN N)) Summary Form: ( DEFMACRO FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 >>(DEFUN BAR NIL (DECLARE (XARGS :GUARD T)) (FOO 26)) Since BAR is non-recursive, its admission is trivial. We observe that the type of BAR is described by the theorem (AND (INTEGERP (BAR)) (< 0 (BAR))). Computing the guard conjecture for BAR.... The guard conjecture for BAR is trivial to prove. BAR is compliant with Common Lisp. Summary Form: ( DEFUN BAR ...) Rules: NIL Warnings: None Time: 2.24 seconds (prove: 0.00, print: 0.00, other: 2.24) BAR * 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 "speed-test1" ...) Rules: NIL Warnings: None Time: 2.21 seconds (prove: 0.00, print: 0.00, other: 2.21) * Step 4: Write the certificate for "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test1.lisp" in "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test1.cert" , and compile the expansion file, /v/filer4b/v41q001/moore/public_html/acl2/se\ minar/2010.05-12-kaufmann/hcomp-tests/speed-test1@expansion.lsp. * Step 5: Compiling the functions defined in "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test1.lisp". Writing book expansion file, /v/filer4b/v41q001/moore/public_html/acl2/seminar\ /2010.05-12-kaufmann/hcomp-tests/speed-test1@expansion.lsp. "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test1.lx64fsl" Note: Deleting book expansion file, /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/speed-test1@expansion.lsp. Summary Form: (CERTIFY-BOOK "speed-test1" ...) Rules: NIL Warnings: None Time: 5.60 seconds (prove: 0.00, print: 0.00, other: 5.60) (EV-REC (FARGN FORM 6) ALIST W ...) took 5,616,916 microseconds (5.616916 seconds) to run with 24 available CPU cores. During that period, 5,604,350 microseconds (5.604350 seconds) were spent in user mode 8,001 microseconds (0.008001 seconds) were spent in system mode 873,712 bytes of memory allocated. 7,997 minor page faults, 0 major page faults, 0 swaps. "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test1.lisp" ACL2 !>(quit) > acl2c 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 !>(time$ (include-book "speed-test1")) ; 1.4s (but about 2.5s in 3.6.1) Summary Form: ( INCLUDE-BOOK "speed-test1" ...) Rules: NIL Warnings: None Time: 1.24 seconds (prove: 0.00, print: 0.00, other: 1.24) (EV-REC (FARGN FORM 6) ALIST W ...) took 1,250,822 microseconds (1.250822 seconds) to run with 24 available CPU cores. During that period, 1,248,078 microseconds (1.248078 seconds) were spent in user mode 0 microseconds (0.000000 seconds) were spent in system mode 172,368 bytes of memory allocated. 928 minor page faults, 0 major page faults, 0 swaps. "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test1.lisp" ACL2 !>";;; NOTE: Almost all of the above time is probably translate!" ";;; NOTE: Almost all of the above time is probably translate!" ACL2 !>(ubt! 1) 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(time$ (certify-book "speed-test2")) ; has taken 7.4s (2.5s in 3.6.1) CERTIFICATION ATTEMPT FOR "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test2.lisp" ACL2 Version 3.6.1 * Step 1: Read "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test2.lisp" and compute its check sum. * Step 2: There were four 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-FN (N) (DECLARE (XARGS :GUARD (NATP N))) (IF (ZP N) 1 (1- (+ (FOO-FN (1- N)) (FOO-FN (1- N)))))) The admission of FOO-FN is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). We observe that the type of FOO-FN is described by the theorem (INTEGERP (FOO-FN N)). We used primitive type reasoning. Computing the guard conjecture for FOO-FN.... The guard conjecture for FOO-FN is trivial to prove, given the :compound- recognizer rules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription rule FOO-FN. FOO-FN is compliant with Common Lisp. Summary Form: ( DEFUN FOO-FN ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION FOO-FN)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO-FN ACL2 >>(DEFMACRO FOO (N) (FOO-FN N)) Summary Form: ( DEFMACRO FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 >>(DEFCONST *BAR* (FOO 26)) Summary Form: ( DEFCONST *BAR* ...) Rules: NIL Warnings: None Time: 1.12 seconds (prove: 0.00, print: 0.00, other: 1.12) *BAR* * 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 "speed-test2" ...) Rules: NIL Warnings: None Time: 1.10 seconds (prove: 0.00, print: 0.00, other: 1.10) * Step 4: Write the certificate for "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test2.lisp" in "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test2.cert" , and compile the expansion file, /v/filer4b/v41q001/moore/public_html/acl2/se\ minar/2010.05-12-kaufmann/hcomp-tests/speed-test2@expansion.lsp. * Step 5: Compiling the functions defined in "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test2.lisp". Writing book expansion file, /v/filer4b/v41q001/moore/public_html/acl2/seminar\ /2010.05-12-kaufmann/hcomp-tests/speed-test2@expansion.lsp. "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test2.lx64fsl" Note: Deleting book expansion file, /v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp- tests/speed-test2@expansion.lsp. Summary Form: (CERTIFY-BOOK "speed-test2" ...) Rules: NIL Warnings: None Time: 5.56 seconds (prove: 0.00, print: 0.00, other: 5.56) (EV-REC (FARGN FORM 6) ALIST W ...) took 5,597,627 microseconds (5.597627 seconds) to run with 24 available CPU cores. During that period, 5,544,346 microseconds (5.544346 seconds) were spent in user mode 16,001 microseconds (0.016001 seconds) were spent in system mode 928,768 bytes of memory allocated. 7,170 minor page faults, 0 major page faults, 0 swaps. "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test2.lisp" ACL2 !>(quit) > acl2c 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 !>(time$ (include-book "speed-test2")) ; 0.03 sec (1.2 secs. in 3.6.1) Summary Form: ( INCLUDE-BOOK "speed-test2" ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) (EV-REC (FARGN FORM 6) ALIST W ...) took 8,430 microseconds (0.008430 seconds) to run with 24 available CPU cores. During that period, 8,001 microseconds (0.008001 seconds) were spent in user mode 0 microseconds (0.000000 seconds) were spent in system mode 165,696 bytes of memory allocated. 957 minor page faults, 0 major page faults, 0 swaps. "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/hcomp-tests/speed-test2.lisp" ACL2 !>