~/acl2/acl2$ acl2 Welcome to Clozure Common Lisp Version 1.12-dev/v1.12-dev.1-3-g1944cfb (DarwinX8664)! ACL2 Version 8.1 built October 31, 2018 15:18:01. Copyright (C) 2018, Regents of the University of Texas ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the LICENSE file distributed with ACL2. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + WARNING: This is NOT an ACL2 release; it is a development snapshot + + (git commit hash: f6e1734a215649017f7a23eb4524f9dc881b720e). + + On rare occasions development snapshots may be incomplete, fragile, + + or unable to pass the usual regression tests. + +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.1. Level 1. Cbd "/Users/kaufmann/acl2/acl2/". System books directory "/Users/kaufmann/acl2/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(include-book "centaur/memoize/old" :dir :system) ACL2 Error in ( INCLUDE-BOOK "centaur/memoize/old" ...): The file "/Users/kaufmann/acl2/acl2/books/centaur/memoize/old.lisp" does not exist. Summary Form: ( INCLUDE-BOOK "centaur/memoize/old" ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( INCLUDE-BOOK "centaur/memoize/old" ...): See :DOC failure. ******** FAILED ******** ACL2 !>(include-book "centaur/memoize/old/profile" :dir :system) TTAG NOTE (for included book): Adding ttag :PROFILE from book /Users/kaufmann/acl2/acl2/books/centaur/memoize/old/profile. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "centaur/memoize/old/profile" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/acl2/acl2/books/centaur/memoize/old/profile". Summary Form: ( INCLUDE-BOOK "centaur/memoize/old/profile" ...) Rules: NIL Warnings: Ttags Time: 0.24 seconds (prove: 0.00, print: 0.00, other: 0.24) "/Users/kaufmann/acl2/acl2/books/centaur/memoize/old/profile.lisp" ACL2 !>(profile-acl2) Profiling 5,323 functions. ACL2 Observation in MEMOIZE-CALL-ARRAY-GROW: Now reinitializing memoization structures. This will erase saved values and statistics. (clear-memoize-statistics) invoked. 5323 functions newly profiled. NIL ACL2 !>(include-book "centaur/gl/gl" :dir :system) Note (from clause-processors/equality): disabling DISJOIN, DISJOIN2, CONJOIN and CONJOIN2. Summary Form: ( INCLUDE-BOOK "centaur/gl/gl" ...) Rules: NIL Time: 12.96 seconds (prove: 0.00, print: 0.02, other: 12.94) "/Users/kaufmann/acl2/acl2/books/centaur/gl/gl.lisp" ACL2 !>(memsum) Sorted by *memoize-summary-order-list* = (TOTAL-TIME NUMBER-OF-CALLS). Reporting on 100 of 1,693 functions because *memoize-summary-limit* = 100. (READ-OBJECT Calls 9.65E+3 Time of all outermost calls 208.81 Time per call 0.02 Heap bytes allocated 5.60E+7; 0.5% Heap bytes allocated per call 5.80E+3 To self/unprofiled functions 2.09E+2; 100.0% To other functions 1.89E+4 calls took 1.52E-3; <0.01% From READ-STANDARD-OI 2.00E+0 calls took 2.08E+2; 99.5% From other functions 9.64E+3 calls took 1.05E+0; 0.5%) (LD-READ-COMMAND Calls 2 Time of all outermost calls 207.76 Time per call 103.88 Heap bytes allocated 2.13E+3; 0.0% Heap bytes allocated per call 1.06E+3 To READ-STANDARD-OI 2.00E+0 calls took 2.08E+2; 100.0% To self/unprofiled functions 2.86E-5; <0.01% To other functions 8.00E+0 calls took 9.98E-6; <0.01% From LD-READ-EVAL-PRINT 2.00E+0 calls took 2.08E+2; 100.0%) (READ-STANDARD-OI Calls 2 Time of all outermost calls 207.76 Time per call 103.88 Heap bytes allocated 2.13E+3; 0.0% Heap bytes allocated per call 1.06E+3 To READ-OBJECT 2.00E+0 calls took 2.08E+2; 100.0% To other functions 2.00E+0 calls took 7.90E-8; <0.01% From LD-READ-COMMAND 2.00E+0 calls took 2.08E+2; 100.0%) (LD-READ-EVAL-PRINT Calls (running) 2 Time of all outermost calls 30.35 Time per call 15.17 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 2.99E+8 To LD-READ-COMMAND 2.00E+0 calls took 2.08E+2; 684.6% To TRANS-EVAL-DEFAULT-WARNING 2.00E+0 calls took 1.28E+1; 42.1% To other functions 2.70E+1 calls took 1.84E-4; <0.01% From other functions 2.00E+0 calls took 3.03E+1; 100.0%) (TRANS-EVAL-DEFAULT-WARNING Calls (running) 782 Time of all outermost calls 12.79 Time per call 0.02 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 7.63E+5 To TRANS-EVAL0 2.00E+0 calls took 1.28E+1; 100.0% To self/unprofiled functions 1.91E-6; <0.01% From LD-READ-EVAL-PRINT 2.00E+0 calls took 1.28E+1; 100.0%) (TRANS-EVAL0 Calls (running) 2.75E+4 Time of all outermost calls 12.79 Time per call 4.66E-4 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 2.17E+4 To TRANS-EVAL1 2.00E+0 calls took 1.28E+1; 100.0% To other functions 8.00E+0 calls took 1.98E-4; <0.01% From TRANS-EVAL-DEFAULT-WARNING 2.00E+0 calls took 1.28E+1; 100.0%) (EV-REC Calls (running) 3.38E+6 Time of all outermost calls 12.79 Time per call 3.78E-6 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 176.67 To EV-FNCALL-REC 3.00E+0 calls took 1.28E+1; 100.0% To other functions 6.00E+0 calls took 5.43E-5; <0.01% To self/unprofiled functions 2.86E-6; <0.01% From EV 2.00E+0 calls took 1.28E+1; 100.0% From other functions 3.38E+6 calls took 5.40E-5; ?%) (EV-FNCALL-REC Calls (running) 1.44E+6 Time of all outermost calls 12.79 Time per call 8.86E-6 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 413.45 To INCLUDE-BOOK-FN 1.00E+0 calls took 1.28E+1; 100.0% To self/unprofiled functions 1.98E-5; <0.01% To other functions 1.26E+2 calls took 1.68E-5; <0.01% From EV-REC 3.00E+0 calls took 1.28E+1; 100.0% From other functions 1.44E+6 calls took 2.59E-5; ?%) (TRANS-EVAL1 Calls (running) 3.94E+4 Time of all outermost calls 12.79 Time per call 3.25E-4 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 1.52E+4 To EV-FOR-TRANS-EVAL 2.00E+0 calls took 1.28E+1; 100.0% To other functions 4.00E+0 calls took 8.08E-6; <0.01% From TRANS-EVAL0 2.00E+0 calls took 1.28E+1; 100.0%) (EV-FOR-TRANS-EVAL Calls (running) 3.94E+4 Time of all outermost calls 12.79 Time per call 3.25E-4 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 1.52E+4 To EV 2.00E+0 calls took 1.28E+1; 100.0% To other functions 8.00E+0 calls took 6.51E-6; <0.01% To self/unprofiled functions 1.79E-6; <0.01% From TRANS-EVAL1 2.00E+0 calls took 1.28E+1; 100.0%) (EV Calls (running) 5.86E+4 Time of all outermost calls 12.79 Time per call 2.18E-4 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 1.02E+4 To EV-REC 2.00E+0 calls took 1.28E+1; 100.0% To other functions 6.00E+0 calls took 2.29E-6; <0.01% To self/unprofiled functions 9.54E-7; <0.01% From EV-FOR-TRANS-EVAL 2.00E+0 calls took 1.28E+1; 100.0%) (INCLUDE-BOOK-FN Calls 1.36E+3 Time of all outermost calls 12.79 Time per call 9.40E-3 Heap bytes allocated 5.97E+8; 5.3% Heap bytes allocated per call 4.39E+5 To INCLUDE-BOOK-FN1 1.00E+0 calls took 1.15E+1; 90.1% To self/unprofiled functions 9.00E-1; 7.0% To PARSE-BOOK-NAME 1.36E+3 calls took 1.96E-1; 1.5% To other functions 1.12E+4 calls took 1.73E-1; 1.4% From EV-FNCALL-REC 1.00E+0 calls took 1.28E+1; 100.0%) (INCLUDE-BOOK-FN1 Calls 1.36E+3 Time of all outermost calls 11.52 Time per call 8.47E-3 Heap bytes allocated 5.50E+8; 4.9% Heap bytes allocated per call 4.04E+5 To PROCESS-EMBEDDED-EVENTS 1.00E+0 calls took 1.11E+1; 96.0% To CHK-CERTIFICATE-FILE 1.00E+0 calls took 4.54E-1; 3.9% To other functions 4.40E+1 calls took 7.55E-3; 0.1% To self/unprofiled functions 2.48E-5; <0.01% From INCLUDE-BOOK-FN 1.00E+0 calls took 1.15E+1; 100.0%) (PROCESS-EMBEDDED-EVENTS Calls 1.73E+3 Time of all outermost calls 11.21 Time per call 6.46E-3 Heap bytes allocated 5.18E+8; 4.6% Heap bytes allocated per call 2.99E+5 To EVAL-EVENT-LST 1.90E+1 calls took 1.12E+1; 100.0% To other functions 2.85E+2 calls took 1.92E-3; 0.0% To self/unprofiled functions 1.49E-4; <0.01% From INCLUDE-BOOK-FN1 1.00E+0 calls took 1.11E+1; 98.7% From CHK-RAISE-PORTCULLIS2 1.80E+1 calls took 1.50E-1; 1.3%) (EVAL-EVENT-LST Calls 6.69E+3 Time of all outermost calls 11.21 Time per call 1.67E-3 Heap bytes allocated 5.18E+8; 4.6% Heap bytes allocated per call 7.74E+4 To TRANS-EVAL-NO-WARNING 1.75E+2 calls took 1.12E+1; 100.0% To other functions 1.46E+3 calls took 4.02E-3; 0.0% To self/unprofiled functions 2.53E-4; <0.01% From PROCESS-EMBEDDED-EVENTS 1.90E+1 calls took 1.12E+1; 100.0%) (TRANS-EVAL-NO-WARNING Calls 2.67E+4 Time of all outermost calls 11.20 Time per call 4.20E-4 Heap bytes allocated 5.18E+8; 4.6% Heap bytes allocated per call 1.94E+4 To PROGN-FN 1.36E+3 calls took 5.11E+0; 45.6% To DEFUN-FN 1.24E+3 calls took 1.49E+0; 13.3% To CHK-CERTIFICATE-FILE 2.04E+2 calls took 1.13E+0; 10.1% To ENCAPSULATE-FN 2.14E+2 calls took 1.07E+0; 9.5% To other functions 2.41E+5 calls took 6.93E-1; 6.2% To READ-OBJECT-FILE 2.04E+2 calls took 5.90E-1; 5.3% To CHK-EMBEDDED-EVENT-FORM 5.67E+3 calls took 2.72E-1; 2.4% To CHK-INPUT-OBJECT-FILE 6.26E+2 calls took 2.12E-1; 1.9% To DEFTHM-FN 9.29E+2 calls took 2.07E-1; 1.8% To ACCUMULATE-POST-ALIST 2.04E+2 calls took 1.31E-1; 1.2% To MACROEXPAND1* 6.37E+3 calls took 1.27E-1; 1.1% To IN-THEORY-FN 1.46E+2 calls took 1.21E-1; 1.1% To self/unprofiled functions 4.56E-2; 0.4% From EVAL-EVENT-LST 1.75E+2 calls took 1.12E+1; 100.0%) (PROGN-FN Calls 4.96E+3 Time of all outermost calls 5.70 Time per call 1.15E-3 Heap bytes allocated 2.73E+8; 2.4% Heap bytes allocated per call 5.50E+4 To PROGN-FN1 1.61E+3 calls took 5.70E+0; 100.0% To self/unprofiled functions 8.33E-4; 0.0% From TRANS-EVAL-NO-WARNING 1.36E+3 calls took 5.11E+0; 89.8% From ENCAPSULATE-PASS-2 1.63E+3 calls took 5.82E-1; 10.2%) (PROGN-FN1 Calls 4.96E+3 Time of all outermost calls 5.70 Time per call 1.15E-3 Heap bytes allocated 2.73E+8; 2.4% Heap bytes allocated per call 5.50E+4 To ENCAPSULATE-FN 1.09E+3 calls took 3.22E+0; 56.6% To TABLE-FN 2.81E+3 calls took 4.37E-1; 7.7% To DEFUN-FN 3.92E+2 calls took 3.63E-1; 6.4% To MACROEXPAND1* 1.74E+4 calls took 2.90E-1; 5.1% To other functions 6.21E+5 calls took 2.81E-1; 4.9% To CHK-EMBEDDED-EVENT-FORM 1.10E+4 calls took 2.36E-1; 4.1% To TRANSLATE1 1.07E+4 calls took 2.32E-1; 4.1% To DEFTHM-FN 9.26E+2 calls took 1.65E-1; 2.9% To DEFUNS-FN 2.70E+1 calls took 1.64E-1; 2.9% To IN-THEORY-FN 5.82E+2 calls took 1.10E-1; 1.9% To TRANSLATE 6.72E+3 calls took 1.07E-1; 1.9% To self/unprofiled functions 8.55E-2; 1.5% From PROGN-FN 1.61E+3 calls took 5.70E+0; 100.0%) (ENCAPSULATE-FN Calls 1.51E+3 Time of all outermost calls 4.30 Time per call 2.85E-3 Heap bytes allocated 2.20E+8; 2.0% Heap bytes allocated per call 1.46E+5 To ENCAPSULATE-PASS-2 1.19E+3 calls took 4.20E+0; 97.8% To other functions 2.99E+4 calls took 8.66E-2; 2.0% To self/unprofiled functions 8.13E-3; 0.2% From PROGN-FN1 1.09E+3 calls took 3.22E+0; 75.0% From TRANS-EVAL-NO-WARNING 2.14E+2 calls took 1.07E+0; 24.9% From other functions 2.06E+2 calls took 5.29E-3; 0.1%) (ENCAPSULATE-PASS-2 Calls 1.50E+3 Time of all outermost calls 4.20 Time per call 2.80E-3 Heap bytes allocated 2.14E+8; 1.9% Heap bytes allocated per call 1.43E+5 To DEFUN-FN 8.56E+2 calls took 8.96E-1; 21.3% To TABLE-FN 2.25E+3 calls took 6.59E-1; 15.7% To DEFTHM-FN 3.14E+3 calls took 6.30E-1; 15.0% To PROGN-FN 1.63E+3 calls took 5.82E-1; 13.8% To MACROEXPAND1* 1.47E+4 calls took 2.75E-1; 6.5% To other functions 5.38E+5 calls took 2.63E-1; 6.2% To IN-THEORY-FN 9.11E+2 calls took 2.40E-1; 5.7% To TRANSLATE1 1.07E+4 calls took 2.22E-1; 5.3% To CHK-EMBEDDED-EVENT-FORM 1.29E+4 calls took 9.48E-2; 2.3% To DEFMACRO-FN 5.45E+2 calls took 8.89E-2; 2.1% To self/unprofiled functions 7.93E-2; 1.9% To NEW-TRIPS 1.46E+3 calls took 7.09E-2; 1.7% To TRANSLATE 4.00E+3 calls took 5.83E-2; 1.4% To DEFTHEORY-FN 5.00E+0 calls took 4.63E-2; 1.1% From ENCAPSULATE-FN 1.19E+3 calls took 4.20E+0; 100.0%) (DEFUNS-FN Calls 2.70E+3 Time of all outermost calls 3.08 Time per call 1.14E-3 Heap bytes allocated 1.18E+8; 1.1% Heap bytes allocated per call 4.37E+4 To DEFUNS-FN0 2.67E+3 calls took 1.66E+0; 54.0% To CHK-ACCEPTABLE-DEFUNS 2.70E+3 calls took 1.00E+0; 32.6% To INSTALL-EVENT-DEFUNS 2.67E+3 calls took 3.04E-1; 9.9% To PRINT-SUMMARY 2.70E+3 calls took 4.88E-2; 1.6% To INITIALIZE-SUMMARY-ACCUMULATORS 2.70E+3 calls took 3.16E-2; 1.0% To self/unprofiled functions 2.07E-2; 0.7% To other functions 4.05E+4 calls took 9.74E-3; 0.3% From DEFUN-FN 2.60E+3 calls took 2.79E+0; 90.7% From PROGN-FN1 2.70E+1 calls took 1.64E-1; 5.3% From TRANS-EVAL-NO-WARNING 6.80E+1 calls took 1.08E-1; 3.5% From other functions 9.00E+0 calls took 1.45E-2; 0.5%) (DEFUN-FN Calls 2.60E+3 Time of all outermost calls 2.79 Time per call 1.08E-3 Heap bytes allocated 1.07E+8; 1.0% Heap bytes allocated per call 4.11E+4 To DEFUNS-FN 2.60E+3 calls took 2.79E+0; 100.0% To self/unprofiled functions 1.37E-3; 0.0% From TRANS-EVAL-NO-WARNING 1.24E+3 calls took 1.49E+0; 53.3% From ENCAPSULATE-PASS-2 8.56E+2 calls took 8.96E-1; 32.1% From PROGN-FN1 3.92E+2 calls took 3.63E-1; 13.0% From DEFSTOBJ-FN 7.20E+1 calls took 3.40E-2; 1.2% From other functions 3.80E+1 calls took 1.11E-2; 0.4%) (TRANSLATE1-CMP Calls 7.38E+4 Time of all outermost calls 2.17 Time per call 2.94E-5 Heap bytes allocated 8.37E+7; 0.7% Heap bytes allocated per call 1.13E+3 To TRANSLATE11 7.38E+4 calls took 2.15E+0; 98.9% To self/unprofiled functions 2.38E-2; 1.1% From TRANSLATE1 3.02E+4 calls took 7.99E-1; 36.8% From TRANSLATE-BODIES1 2.82E+3 calls took 7.78E-1; 35.8% From TRANSLATE-CMP 4.08E+4 calls took 5.95E-1; 27.4%) (TRANSLATE11 Calls 5.35E+5 Time of all outermost calls 2.15 Time per call 4.02E-6 Heap bytes allocated 8.37E+7; 0.7% Heap bytes allocated per call 156.43 To TRANSLATE11-LET 3.52E+3 calls took 9.88E-1; 46.0% To TRANSLATE11-CALL 5.26E+4 calls took 4.93E-1; 23.0% To MACROEXPAND1-CMP 2.27E+4 calls took 2.23E-1; 10.4% To TRANSLATE11-LST 8.62E+3 calls took 1.48E-1; 6.9% To self/unprofiled functions 1.27E-1; 5.9% To other functions 5.42E+5 calls took 7.85E-2; 3.7% To TRANSLATE11-MV-LET 4.96E+2 calls took 5.59E-2; 2.6% To FGETPROP 2.43E+5 calls took 3.35E-2; 1.6% From TRANSLATE1-CMP 7.38E+4 calls took 2.15E+0; 100.0%) (MACROEXPAND1-CMP Calls 1.69E+5 Time of all outermost calls 2.10 Time per call 1.25E-5 Heap bytes allocated 9.92E+7; 0.9% Heap bytes allocated per call 588.46 To EV-W 3.37E+5 calls took 1.68E+0; 79.7% To BIND-MACRO-ARGS 1.69E+5 calls took 2.18E-1; 10.4% To self/unprofiled functions 1.11E-1; 5.3% To GUARD 1.69E+5 calls took 4.53E-2; 2.2% To MACRO-ARGS 1.69E+5 calls took 3.21E-2; 1.5% To other functions 3.37E+5 calls took 1.98E-2; 0.9% From MACROEXPAND1*-CMP 5.08E+4 calls took 6.32E-1; 30.1% From MACROEXPAND1 6.28E+3 calls took 5.60E-1; 26.6% From TRANSLATE11-LST 3.08E+4 calls took 2.35E-1; 11.2% From TRANSLATE11 2.27E+4 calls took 2.23E-1; 10.6% From TRANSLATE11-MV-LET 2.69E+4 calls took 1.93E-1; 9.2% From TRANSLATE11-LET 2.22E+4 calls took 1.75E-1; 8.3% From TRANSLATE11-CALL-1 8.25E+3 calls took 7.50E-2; 3.6% From other functions 7.83E+2 calls took 9.21E-3; 0.4%) (EV-W Calls 3.37E+5 Time of all outermost calls 1.68 Time per call 4.97E-6 Heap bytes allocated 8.68E+7; 0.8% Heap bytes allocated per call 257.40 To EV-REC-LST 3.00E+5 calls took 8.94E-1; 53.3% To self/unprofiled functions 4.21E-1; 25.1% To ALISTP 3.91E+6 calls took 9.04E-2; 5.4% To other functions 1.49E+6 calls took 6.70E-2; 4.0% To TRANSLATED-ACL2-UNWIND-PROTECTP 3.92E+5 calls took 5.61E-2; 3.3% To ASSOC-EQUAL 1.26E+6 calls took 3.91E-2; 2.3% To ASSOC-EQL-EXEC 1.24E+6 calls took 3.68E-2; 2.2% To FGETPROP 2.79E+5 calls took 2.85E-2; 1.7% To STOBJS-OUT 2.76E+5 calls took 2.70E-2; 1.6% To ASSOC-EQL-EXEC$GUARD-CHECK 1.24E+6 calls took 1.75E-2; 1.0% From MACROEXPAND1-CMP 3.37E+5 calls took 1.68E+0; 100.0% From other functions 4.00E+0 calls took 6.31E-5; ?%) (DEFUNS-FN0 Calls 2.67E+3 Time of all outermost calls 1.66 Time per call 6.24E-4 Heap bytes allocated 6.02E+7; 0.5% Heap bytes allocated per call 2.26E+4 To DEFUNS-FN1 1.83E+3 calls took 1.24E+0; 74.8% To PUT-INDUCTION-INFO 1.83E+3 calls took 4.10E-1; 24.6% To other functions 2.67E+3 calls took 7.25E-3; 0.4% To self/unprofiled functions 2.29E-3; 0.1% From DEFUNS-FN 2.67E+3 calls took 1.66E+0; 100.0%) (INSTALL-EVENT Calls 1.75E+4 Time of all outermost calls 1.63 Time per call 9.34E-5 Heap bytes allocated 7.90E+7; 0.7% Heap bytes allocated per call 4.52E+3 To SET-W 3.49E+4 calls took 1.18E+0; 72.2% To TAU-VISIT-EVENT 1.75E+4 calls took 3.20E-1; 19.6% To ADD-EVENT-LANDMARK 1.75E+4 calls took 7.37E-2; 4.5% To self/unprofiled functions 3.75E-2; 2.3% To other functions 1.61E+5 calls took 2.25E-2; 1.4% From TABLE-FN1 5.18E+3 calls took 7.51E-1; 46.1% From DEFTHM-FN1 4.86E+3 calls took 2.99E-1; 18.4% From INSTALL-EVENT-DEFUNS 2.67E+3 calls took 2.99E-1; 18.4% From IN-THEORY-FN 1.53E+3 calls took 1.42E-1; 8.7% From other functions 2.04E+3 calls took 5.09E-2; 3.1% From DEFPKG-FN 2.80E+1 calls took 4.72E-2; 2.9% From DEFMACRO-FN 1.16E+3 calls took 4.10E-2; 2.5%) (CHK-CERTIFICATE-FILE Calls 223 Time of all outermost calls 1.58 Time per call 7.10E-3 Heap bytes allocated 1.20E+8; 1.1% Heap bytes allocated per call 5.39E+5 To CHK-CERTIFICATE-FILE1 2.01E+2 calls took 1.34E+0; 84.5% To CHK-IN-PACKAGE 2.01E+2 calls took 1.26E-1; 8.0% To SET-CBD-STATE 4.02E+2 calls took 6.53E-2; 4.1% To CERTIFICATE-FILE-AND-INPUT-CHANNEL 2.01E+2 calls took 3.08E-2; 1.9% To CLOSE-INPUT-CHANNEL 2.01E+2 calls took 2.25E-2; 1.4% To self/unprofiled functions 1.28E-3; 0.1% To other functions 2.01E+2 calls took 1.12E-5; <0.01% From TRANS-EVAL-NO-WARNING 2.04E+2 calls took 1.13E+0; 71.3% From INCLUDE-BOOK-FN1 1.00E+0 calls took 4.54E-1; 28.7%) (CHK-CERTIFICATE-FILE1 Calls 223 Time of all outermost calls 1.34 Time per call 6.00E-3 Heap bytes allocated 1.16E+8; 1.0% Heap bytes allocated per call 5.18E+5 To CHK-RAISE-PORTCULLIS 2.01E+2 calls took 1.33E+0; 99.6% To other functions 4.02E+2 calls took 4.99E-3; 0.4% To self/unprofiled functions 5.67E-4; 0.0% From CHK-CERTIFICATE-FILE 2.01E+2 calls took 1.34E+0; 100.0%) (CHK-RAISE-PORTCULLIS Calls 223 Time of all outermost calls 1.33 Time per call 5.98E-3 Heap bytes allocated 1.15E+8; 1.0% Heap bytes allocated per call 5.18E+5 To CHK-RAISE-PORTCULLIS1 2.01E+2 calls took 9.24E-1; 69.4% To READ-FILE-INTO-TEMPLATE 2.01E+2 calls took 3.41E-1; 25.6% To SYSFILE-TO-FILENAME-INCLUDE-BOOK-ALIST 4.02E+2 calls took 5.09E-2; 3.8% To INCLUDE-BOOK-ALIST-SUBSETP 2.01E+2 calls took 1.51E-2; 1.1% To self/unprofiled functions 1.08E-3; 0.1% To other functions 8.04E+2 calls took 4.05E-4; 0.0% From CHK-CERTIFICATE-FILE1 2.01E+2 calls took 1.33E+0; 100.0%) (SET-W Calls 4.29E+4 Time of all outermost calls 1.29 Time per call 3.00E-5 Heap bytes allocated 8.13E+7; 0.7% Heap bytes allocated per call 1.89E+3 To self/unprofiled functions 9.91E-1; 77.0% To INSTALL-GLOBAL-ENABLED-STRUCTURE 4.29E+4 calls took 1.33E-1; 10.3% To RECOMPRESS-STOBJ-ACCESSOR-ARRAYS 4.29E+4 calls took 1.03E-1; 8.0% To UNION-EQ-EXEC 3.10E+1 calls took 3.33E-2; 2.6% To other functions 1.82E+5 calls took 2.72E-2; 2.1% From INSTALL-EVENT 3.49E+4 calls took 1.18E+0; 91.4% From DEFUNS-FN1 1.85E+3 calls took 5.68E-2; 4.4% From ENCAPSULATE-PASS-2 3.05E+3 calls took 1.98E-2; 1.5% From other functions 2.27E+3 calls took 1.85E-2; 1.4% From PUT-INDUCTION-INFO 7.96E+2 calls took 1.58E-2; 1.2%) (DEFUNS-FN1 Calls 1.83E+3 Time of all outermost calls 1.24 Time per call 6.81E-4 Heap bytes allocated 3.80E+7; 0.3% Heap bytes allocated per call 2.08E+4 To PUTPROP-BODY-LST 1.83E+3 calls took 1.10E+0; 88.7% To SET-W 1.85E+3 calls took 5.68E-2; 4.6% To other functions 3.34E+4 calls took 4.02E-2; 3.2% To PUTPROP-LEVEL-NO-LST 1.83E+3 calls took 2.11E-2; 1.7% To PUTPROP-HEREDITARILY-CONSTRAINED-FNNAMES-/// 1.83E+3 calls took 1.43E-2; 1.1% To self/unprofiled functions 7.85E-3; 0.6% From DEFUNS-FN0 1.83E+3 calls took 1.24E+0; 100.0%) (TABLE-FN Calls 5.70E+3 Time of all outermost calls 1.15 Time per call 2.03E-4 Heap bytes allocated 6.70E+7; 0.6% Heap bytes allocated per call 1.18E+4 To TABLE-FN1 5.70E+3 calls took 9.79E-1; 84.8% To SIMPLE-TRANSLATE-AND-EVAL 1.14E+4 calls took 1.68E-1; 14.6% To self/unprofiled functions 6.68E-3; 0.6% To other functions 1.14E+4 calls took 8.12E-4; 0.1% From ENCAPSULATE-PASS-2 2.25E+3 calls took 6.59E-1; 57.1% From PROGN-FN1 2.81E+3 calls took 4.37E-1; 37.9% From TRANS-EVAL-NO-WARNING 2.90E+2 calls took 2.64E-2; 2.3% From MAYBE-INSTALL-ACL2-DEFAULTS-TABLE 1.32E+2 calls took 2.06E-2; 1.8% From other functions 2.13E+2 calls took 1.12E-2; 1.0%) (EV-REC-LST Calls 1.48E+6 Time of all outermost calls 1.13 Time per call 7.66E-7 Heap bytes allocated 7.75E+7; 0.7% Heap bytes allocated per call 52.33 To self/unprofiled functions 6.41E-1; 56.5% To other functions 5.46E+6 calls took 9.08E-2; 8.0% To TRANSLATED-ACL2-UNWIND-PROTECTP 1.13E+6 calls took 8.59E-2; 7.6% To FGETPROP 1.10E+6 calls took 7.89E-2; 7.0% To EV-REC-RETURN-LAST 4.35E+3 calls took 5.41E-2; 4.8% To UNION-EQ-EXEC 3.30E+1 calls took 4.08E-2; 3.6% To STOBJS-OUT 1.07E+6 calls took 3.91E-2; 3.5% To EV-REC-ACL2-UNWIND-PROTECT 7.00E+0 calls took 3.71E-2; 3.3% To LATCH-STOBJS 1.10E+6 calls took 2.24E-2; 2.0% To W 1.15E+6 calls took 2.00E-2; 1.8% To TRUE-LISTP 1.96E+5 calls took 1.22E-2; 1.1% To UNIVERSAL-THEORY-FN 6.00E+0 calls took 1.16E-2; 1.0% From EV-W 3.00E+5 calls took 8.94E-1; 78.9% From SIMPLE-TRANSLATE-AND-EVAL 3.69E+3 calls took 1.33E-1; 11.7% From TRANS-EVAL-NO-WARNING 6.40E+3 calls took 3.27E-2; 2.9% From ENCAPSULATE-PASS-2 1.43E+4 calls took 2.69E-2; 2.4% From EV-REC-ACL2-UNWIND-PROTECT 4.65E+3 calls took 2.16E-2; 1.9% From PROGN-FN1 1.69E+4 calls took 2.06E-2; 1.8% From other functions 1.13E+6 calls took 5.36E-3; 0.5%) (TRANSLATE11-LET Calls 1.77E+4 Time of all outermost calls 1.11 Time per call 6.27E-5 Heap bytes allocated 5.05E+7; 0.4% Heap bytes allocated per call 2.86E+3 To TRANSLATE11-MV-LET 1.53E+3 calls took 4.79E-1; 43.3% To TRANSLATE11-LST 3.12E+4 calls took 1.87E-1; 16.8% To MACROEXPAND1-CMP 2.22E+4 calls took 1.75E-1; 15.8% To TRANSLATE11-CALL 1.28E+4 calls took 8.56E-2; 7.7% To self/unprofiled functions 6.82E-2; 6.2% To other functions 4.84E+5 calls took 5.79E-2; 5.2% To FGETPROP 1.17E+5 calls took 1.71E-2; 1.5% To COLLECT-DECLARATIONS-CMP 9.52E+3 calls took 1.39E-2; 1.3% To ARGLISTP 9.52E+3 calls took 1.25E-2; 1.1% To MAKE-LAMBDA-TERM 9.48E+3 calls took 1.15E-2; 1.0% From TRANSLATE11 3.52E+3 calls took 9.88E-1; 89.2% From TRANSLATE11-LST 4.44E+3 calls took 6.72E-2; 6.1% From TRANSLATE11-CALL-1 1.06E+3 calls took 3.67E-2; 3.3% From TRANSLATE11-MV-LET 4.68E+3 calls took 1.53E-2; 1.4%) (PUTPROP-BODY-LST Calls 1.83E+3 Time of all outermost calls 1.10 Time per call 6.04E-4 Heap bytes allocated 2.98E+7; 0.3% Heap bytes allocated per call 1.63E+4 To ADD-DEFINITION-RULE-WITH-TTREE 1.95E+3 calls took 1.10E+0; 99.7% To self/unprofiled functions 1.85E-3; 0.2% To other functions 5.84E+3 calls took 9.58E-4; 0.1% From DEFUNS-FN1 1.83E+3 calls took 1.10E+0; 100.0%) (ADD-DEFINITION-RULE-WITH-TTREE Calls 1.96E+3 Time of all outermost calls 1.10 Time per call 5.63E-4 Heap bytes allocated 2.97E+7; 0.3% Heap bytes allocated per call 1.52E+4 To DESTRUCTURE-DEFINITION 1.96E+3 calls took 1.09E+0; 98.8% To other functions 1.81E+4 calls took 8.44E-3; 0.8% To self/unprofiled functions 5.10E-3; 0.5% From PUTPROP-BODY-LST 1.95E+3 calls took 1.10E+0; 99.8% From other functions 1.20E+1 calls took 2.22E-3; 0.2%) (DESTRUCTURE-DEFINITION Calls 1.99E+3 Time of all outermost calls 1.09 Time per call 5.48E-4 Heap bytes allocated 2.87E+7; 0.3% Heap bytes allocated per call 1.44E+4 To NORMALIZE 1.91E+3 calls took 1.08E+0; 98.8% To other functions 3.83E+3 calls took 1.11E-2; 1.0% To self/unprofiled functions 2.14E-3; 0.2% From ADD-DEFINITION-RULE-WITH-TTREE 1.96E+3 calls took 1.09E+0; 100.0% From other functions 2.80E+1 calls took 7.74E-6; ?%) (NORMALIZE Calls 3.79E+5 Time of all outermost calls 1.08 Time per call 2.86E-6 Heap bytes allocated 2.83E+7; 0.3% Heap bytes allocated per call 74.76 To NORMALIZE-LST 5.54E+4 calls took 4.10E-1; 37.8% To DISTRIBUTE-FIRST-IF 4.78E+4 calls took 2.93E-1; 27.1% To ASSUME-TRUE-FALSE-BC 4.96E+4 calls took 2.50E-1; 23.1% To TYPE-SET-LST 7.40E+3 calls took 4.62E-2; 4.3% To NOT-IDENT 1.08E+4 calls took 4.39E-2; 4.1% To self/unprofiled functions 2.32E-2; 2.1% To CONS-TERM 8.54E+4 calls took 1.40E-2; 1.3% To other functions 3.54E+4 calls took 2.55E-3; 0.2% From DESTRUCTURE-DEFINITION 1.91E+3 calls took 1.08E+0; 99.4% From other functions 3.77E+5 calls took 6.93E-3; 0.6%) (TABLE-FN1 Calls 5.70E+3 Time of all outermost calls 1.01 Time per call 1.77E-4 Heap bytes allocated 5.72E+7; 0.5% Heap bytes allocated per call 1.00E+4 To INSTALL-EVENT 5.18E+3 calls took 7.51E-1; 74.3% To PRINT-SUMMARY 5.55E+3 calls took 7.63E-2; 7.5% To INITIALIZE-SUMMARY-ACCUMULATORS 5.55E+3 calls took 6.72E-2; 6.7% To CHK-TABLE-GUARD 5.00E+3 calls took 4.60E-2; 4.5% To other functions 8.85E+4 calls took 3.12E-2; 3.1% To self/unprofiled functions 2.71E-2; 2.7% To CHK-TABLE-GUARDS 1.78E+2 calls took 1.22E-2; 1.2% From TABLE-FN 5.70E+3 calls took 9.79E-1; 96.8% From EV-REC-ACL2-UNWIND-PROTECT 7.00E+0 calls took 3.24E-2; 3.2%) (CHK-ACCEPTABLE-DEFUNS Calls 2.70E+3 Time of all outermost calls 1.00 Time per call 3.71E-4 Heap bytes allocated 4.20E+7; 0.4% Heap bytes allocated per call 1.56E+4 To CHK-ACCEPTABLE-DEFUNS1 2.67E+3 calls took 9.30E-1; 92.8% To CHK-DEFUNS-TUPLES 2.70E+3 calls took 2.75E-2; 2.7% To CHK-ACCEPTABLE-DEFUNS0 2.70E+3 calls took 2.37E-2; 2.4% To other functions 1.62E+4 calls took 1.39E-2; 1.4% To self/unprofiled functions 7.33E-3; 0.7% From DEFUNS-FN 2.70E+3 calls took 1.00E+0; 100.0%) (DEFTHM-FN Calls 5.00E+3 Time of all outermost calls 1.00 Time per call 2.00E-4 Heap bytes allocated 4.33E+7; 0.4% Heap bytes allocated per call 8.67E+3 To DEFTHM-FN1 4.94E+3 calls took 9.95E-1; 99.3% To other functions 5.05E+3 calls took 4.01E-3; 0.4% To self/unprofiled functions 2.81E-3; 0.3% From ENCAPSULATE-PASS-2 3.14E+3 calls took 6.30E-1; 62.9% From TRANS-EVAL-NO-WARNING 9.29E+2 calls took 2.07E-1; 20.7% From PROGN-FN1 9.26E+2 calls took 1.65E-1; 16.5%) (DEFTHM-FN1 Calls 4.94E+3 Time of all outermost calls 0.99 Time per call 2.01E-4 Heap bytes allocated 4.33E+7; 0.4% Heap bytes allocated per call 8.77E+3 To INSTALL-EVENT 4.86E+3 calls took 2.99E-1; 30.1% To TRANSLATE 4.94E+3 calls took 2.07E-1; 20.8% To ADD-RULES 4.86E+3 calls took 1.82E-1; 18.3% To PRINT-SUMMARY 4.94E+3 calls took 6.96E-2; 7.0% To INITIALIZE-SUMMARY-ACCUMULATORS 4.94E+3 calls took 6.33E-2; 6.4% To CHK-ACCEPTABLE-RULES 4.86E+3 calls took 5.65E-2; 5.7% To other functions 1.37E+5 calls took 4.52E-2; 4.5% To self/unprofiled functions 4.19E-2; 4.2% To TRANSLATE-RULE-CLASSES 4.94E+3 calls took 1.83E-2; 1.8% To CHK-JUST-NEW-NAME 4.86E+3 calls took 1.08E-2; 1.1% From DEFTHM-FN 4.94E+3 calls took 9.95E-1; 100.0%) (TRANSLATE11-LST Calls 2.50E+5 Time of all outermost calls 0.98 Time per call 3.93E-6 Heap bytes allocated 3.67E+7; 0.3% Heap bytes allocated per call 147.14 To MACROEXPAND1-CMP 3.08E+4 calls took 2.35E-1; 24.0% To self/unprofiled functions 2.03E-1; 20.7% To TRANSLATE11-CALL 5.89E+4 calls took 1.30E-1; 13.3% To TRANSLATE11-CALL-1 4.67E+4 calls took 1.08E-1; 11.0% To TRANSLATE11-LET 4.44E+3 calls took 6.72E-2; 6.8% To other functions 8.46E+5 calls took 5.08E-2; 5.2% To FGETPROP 3.30E+5 calls took 4.68E-2; 4.8% To TRANSLATE11-VAR-OR-QUOTE-EXIT 2.53E+5 calls took 3.94E-2; 4.0% To LEGAL-VARIABLE-OR-CONSTANT-NAMEP 2.53E+5 calls took 3.37E-2; 3.4% To ARITY 1.03E+5 calls took 1.65E-2; 1.7% To STOBJS-IN-OUT 4.68E+4 calls took 1.50E-2; 1.5% To ILKS-PER-ARGUMENT-SLOT 7.97E+4 calls took 1.27E-2; 1.3% To STOBJ-FIELD-FN-OF-STOBJ-TYPE-P 6.01E+4 calls took 1.26E-2; 1.3% To TRANSLATE-DEREF 3.74E+5 calls took 1.03E-2; 1.1% From TRANSLATE11-CALL-1 8.15E+4 calls took 3.15E-1; 32.1% From TRANSLATE11-CALL 2.81E+4 calls took 1.99E-1; 20.3% From TRANSLATE11-LET 3.12E+4 calls took 1.87E-1; 19.0% From TRANSLATE11 8.62E+3 calls took 1.48E-1; 15.1% From TRANSLATE11-MV-LET 1.42E+4 calls took 1.28E-1; 13.0% From other functions 8.61E+4 calls took 4.22E-3; 0.4%) (CHK-ACCEPTABLE-DEFUNS1 Calls 2.67E+3 Time of all outermost calls 0.93 Time per call 3.49E-4 Heap bytes allocated 4.08E+7; 0.4% Heap bytes allocated per call 1.53E+4 To TRANSLATE-BODIES 2.67E+3 calls took 7.83E-1; 84.1% To other functions 6.48E+4 calls took 4.39E-2; 4.7% To TRANSLATE-TERM-LST 5.33E+3 calls took 3.11E-2; 3.3% To self/unprofiled functions 1.78E-2; 1.9% To CHK-ACCEPTABLE-LAMBDA$-TRANSLATIONS 2.67E+3 calls took 1.77E-2; 1.9% To CHK-LOGIC-SUBFUNCTIONS 5.48E+3 calls took 1.31E-2; 1.4% To TRANSLATE-MEASURES 2.67E+3 calls took 1.29E-2; 1.4% To CHK-JUST-NEW-NAMES 2.67E+3 calls took 1.12E-2; 1.2% From CHK-ACCEPTABLE-DEFUNS 2.67E+3 calls took 9.30E-1; 100.0%) (CHK-RAISE-PORTCULLIS1 Calls 223 Time of all outermost calls 0.92 Time per call 4.15E-3 Heap bytes allocated 5.70E+7; 0.5% Heap bytes allocated per call 2.56E+5 To CHK-RAISE-PORTCULLIS2 2.01E+2 calls took 9.23E-1; 99.8% To other functions 2.01E+2 calls took 1.08E-3; 0.1% To self/unprofiled functions 7.15E-4; 0.1% From CHK-RAISE-PORTCULLIS 2.01E+2 calls took 9.24E-1; 100.0%) (CHK-RAISE-PORTCULLIS2 Calls 223 Time of all outermost calls 0.92 Time per call 4.14E-3 Heap bytes allocated 5.69E+7; 0.5% Heap bytes allocated per call 2.55E+5 To CHK-INPUT-OBJECT-FILE 7.33E+2 calls took 2.62E-1; 28.4% To DEFPKG-FN 2.80E+1 calls took 2.02E-1; 21.9% To PROCESS-EMBEDDED-EVENTS 1.80E+1 calls took 1.50E-1; 16.3% To PARSE-BOOK-NAME 7.33E+2 calls took 1.05E-1; 11.4% To other functions 4.01E+4 calls took 4.16E-2; 4.5% To MACROEXPAND1* 7.74E+2 calls took 3.81E-2; 4.1% To READ-OBJECT 1.03E+3 calls took 2.61E-2; 2.8% To self/unprofiled functions 1.63E-2; 1.8% To TRANSLATE1 7.74E+2 calls took 1.58E-2; 1.7% To READ-OBJECT-FILE 1.80E+1 calls took 1.57E-2; 1.7% To INITIALIZE-SUMMARY-ACCUMULATORS 7.33E+2 calls took 1.51E-2; 1.6% To ASSOC-EQUAL 7.33E+2 calls took 1.35E-2; 1.5% To PRINT-SUMMARY 7.33E+2 calls took 1.16E-2; 1.3% To DEFCONST-FN 1.00E+1 calls took 1.05E-2; 1.1% From CHK-RAISE-PORTCULLIS1 2.01E+2 calls took 9.23E-1; 100.0%) (TRANSLATE1 Calls 3.02E+4 Time of all outermost calls 0.82 Time per call 2.72E-5 Heap bytes allocated 3.46E+7; 0.3% Heap bytes allocated per call 1.14E+3 To TRANSLATE1-CMP 3.02E+4 calls took 7.99E-1; 97.5% To self/unprofiled functions 2.07E-2; 2.5% From TRANSLATE-SIMPLE-OR-ERROR-TRIPLE 2.69E+3 calls took 2.66E-1; 32.5% From PROGN-FN1 1.07E+4 calls took 2.32E-1; 28.3% From ENCAPSULATE-PASS-2 1.07E+4 calls took 2.22E-1; 27.1% From TRANS-EVAL-NO-WARNING 5.17E+3 calls took 8.22E-2; 10.0% From CHK-RAISE-PORTCULLIS2 7.74E+2 calls took 1.58E-2; 1.9% From other functions 1.66E+2 calls took 1.46E-3; 0.2%) (TRANSLATE-BODIES Calls 2.67E+3 Time of all outermost calls 0.78 Time per call 2.94E-4 Heap bytes allocated 3.56E+7; 0.3% Heap bytes allocated per call 1.33E+4 To TRANSLATE-BODIES1 2.67E+3 calls took 7.79E-1; 99.5% To self/unprofiled functions 2.40E-3; 0.3% To other functions 2.76E+3 calls took 1.46E-3; 0.2% From CHK-ACCEPTABLE-DEFUNS1 2.67E+3 calls took 7.83E-1; 100.0%) (TRANSLATE-BODIES1 Calls 2.67E+3 Time of all outermost calls 0.78 Time per call 2.92E-4 Heap bytes allocated 3.51E+7; 0.3% Heap bytes allocated per call 1.32E+4 To TRANSLATE1-CMP 2.82E+3 calls took 7.78E-1; 99.8% To self/unprofiled functions 1.47E-3; 0.2% From TRANSLATE-BODIES 2.67E+3 calls took 7.79E-1; 100.0%) (TRANSLATE11-CALL Calls 1.60E+5 Time of all outermost calls 0.77 Time per call 4.85E-6 Heap bytes allocated 2.79E+7; 0.2% Heap bytes allocated per call 174.76 To TRANSLATE11-CALL-1 4.86E+4 calls took 4.67E-1; 60.3% To TRANSLATE11-LST 2.81E+4 calls took 1.99E-1; 25.7% To STOBJS-IN-OUT 7.67E+4 calls took 5.41E-2; 7.0% To self/unprofiled functions 4.22E-2; 5.4% To ILKS-PER-ARGUMENT-SLOT 2.81E+4 calls took 1.22E-2; 1.6% To other functions 4.49E+2 calls took 7.67E-5; <0.01% From TRANSLATE11 5.26E+4 calls took 4.93E-1; 63.7% From TRANSLATE11-LST 5.89E+4 calls took 1.30E-1; 16.8% From TRANSLATE11-LET 1.28E+4 calls took 8.56E-2; 11.0% From TRANSLATE11-MV-LET 5.43E+3 calls took 6.54E-2; 8.4% From other functions 2.99E+4 calls took 3.43E-4; ?%) (MACROEXPAND1* Calls 3.94E+4 Time of all outermost calls 0.73 Time per call 1.86E-5 Heap bytes allocated 4.20E+7; 0.4% Heap bytes allocated per call 1.07E+3 To MACROEXPAND1*-CMP 3.94E+4 calls took 7.09E-1; 96.8% To self/unprofiled functions 2.36E-2; 3.2% From PROGN-FN1 1.74E+4 calls took 2.90E-1; 39.6% From ENCAPSULATE-PASS-2 1.47E+4 calls took 2.75E-1; 37.5% From TRANS-EVAL-NO-WARNING 6.37E+3 calls took 1.27E-1; 17.4% From CHK-RAISE-PORTCULLIS2 7.74E+2 calls took 3.81E-2; 5.2% From other functions 1.45E+2 calls took 1.99E-3; 0.3%) (MACROEXPAND1*-CMP Calls 3.94E+4 Time of all outermost calls 0.71 Time per call 1.80E-5 Heap bytes allocated 3.76E+7; 0.3% Heap bytes allocated per call 955.51 To MACROEXPAND1-CMP 5.08E+4 calls took 6.32E-1; 89.2% To self/unprofiled functions 4.94E-2; 7.0% To FGETPROP 1.38E+5 calls took 2.26E-2; 3.2% To other functions 9.02E+4 calls took 4.63E-3; 0.7% From MACROEXPAND1* 3.94E+4 calls took 7.09E-1; 100.0%) (FGETPROP Calls 6.75E+6 Time of all outermost calls 0.69 Time per call 1.03E-7 To self/unprofiled functions 6.50E-1; 93.6% To GETPROP-DEFAULT 1.32E+6 calls took 4.48E-2; 6.4% From other functions 7.94E+5 calls took 8.86E-2; 12.8% From EV-REC-LST 1.10E+6 calls took 7.89E-2; 11.4% From TRANSLATE11-LST 3.30E+5 calls took 4.68E-2; 6.7% From GLOBAL-VAL 5.29E+5 calls took 4.59E-2; 6.6% From STOBJS-OUT 5.08E+5 calls took 3.64E-2; 5.2% From TRANSLATE11 2.43E+5 calls took 3.35E-2; 4.8% From TABLE-ALIST 3.84E+5 calls took 3.04E-2; 4.4% From ASSOC-TYPE-ALIST 4.44E+5 calls took 2.99E-2; 4.3% From EV-W 2.79E+5 calls took 2.85E-2; 4.1% From GUARD 1.76E+5 calls took 2.72E-2; 3.9% From CANONICAL-SIBLING 1.87E+5 calls took 2.55E-2; 3.7% From MACROEXPAND1*-CMP 1.38E+5 calls took 2.26E-2; 3.3% From STOBJ-FIELD-FN-OF-STOBJ-TYPE-P 1.67E+5 calls took 2.21E-2; 3.2% From TYPE-SET-REC 1.42E+5 calls took 1.99E-2; 2.9% From ATTACHMENT-ALIST 4.92E+4 calls took 1.90E-2; 2.7% From ARITY 2.44E+5 calls took 1.85E-2; 2.7% From TRANSLATE11-LET 1.17E+5 calls took 1.71E-2; 2.5% From RECOMPRESS-STOBJ-ACCESSOR-ARRAYS 1.13E+5 calls took 1.62E-2; 2.3% From STOBJS-IN 1.44E+5 calls took 1.42E-2; 2.0% From FIND-MAPPING-PAIRS-TAIL 8.05E+4 calls took 1.37E-2; 2.0% From MACRO-ARGS 1.69E+5 calls took 1.33E-2; 1.9% From TRANSLATE11-CALL-1 1.09E+5 calls took 1.29E-2; 1.9% From TRANSLATE11-MV-LET 8.10E+4 calls took 9.27E-3; 1.3% From FUNCTION-SYMBOLP 1.19E+4 calls took 8.49E-3; 1.2% From MACROEXPAND1-CMP 1.69E+5 calls took 8.42E-3; 1.2% From GET-LEVEL-NO 4.39E+4 calls took 7.41E-3; 1.1%) (TYPE-SET-REC Calls 6.68E+5 Time of all outermost calls 0.65 Time per call 9.74E-7 Heap bytes allocated 7.16E+6; 0.1% Heap bytes allocated per call 10.73 To TYPE-SET-WITH-RULES 1.42E+5 calls took 2.72E-1; 41.8% To ASSOC-TYPE-ALIST 5.42E+5 calls took 1.69E-1; 26.0% To self/unprofiled functions 8.78E-2; 13.5% To MOST-RECENT-ENABLED-RECOG-TUPLE 1.54E+5 calls took 4.05E-2; 6.2% To CONS-TAG-TREES 2.55E+5 calls took 2.24E-2; 3.4% To FGETPROP 1.42E+5 calls took 1.99E-2; 3.1% To GLOBAL-VAL 1.54E+5 calls took 1.85E-2; 2.8% To TYPE-SET-FINISH 2.87E+5 calls took 1.16E-2; 1.8% To other functions 6.52E+4 calls took 9.30E-3; 1.4% From TYPE-SET-BC 3.73E+5 calls took 4.54E-1; 69.7% From TYPE-SET 4.16E+4 calls took 6.17E-2; 9.5% From TYPE-SET-LST 3.89E+4 calls took 4.73E-2; 7.3% From ASSUME-TRUE-FALSE-REC 3.44E+4 calls took 3.91E-2; 6.0% From ASSUME-TRUE-FALSE-IF 2.46E+4 calls took 3.47E-2; 5.3% From ASSUME-TRUE-FALSE1 4.23E+3 calls took 1.42E-2; 2.2% From other functions 1.51E+5 calls took 1.77E-5; ?%) (TRANSLATE-CMP Calls 4.08E+4 Time of all outermost calls 0.62 Time per call 1.52E-5 Heap bytes allocated 1.75E+7; 0.2% Heap bytes allocated per call 428.47 To TRANSLATE1-CMP 4.08E+4 calls took 5.95E-1; 96.1% To self/unprofiled functions 1.36E-2; 2.2% To LOGIC-FNSP 6.99E+3 calls took 1.07E-2; 1.7% From TRANSLATE 3.96E+4 calls took 5.80E-1; 93.8% From DEFMACRO-FN 1.18E+3 calls took 3.84E-2; 6.2% From other functions 1.90E+1 calls took 4.49E-5; ?%) (READ-OBJECT-FILE Calls 223 Time of all outermost calls 0.61 Time per call 2.73E-3 Heap bytes allocated 1.27E+7; 0.1% Heap bytes allocated per call 5.72E+4 To READ-OBJECT-FILE1 2.23E+2 calls took 4.41E-1; 72.4% To CHK-IN-PACKAGE 2.23E+2 calls took 1.01E-1; 16.5% To OPEN-INPUT-OBJECT-FILE 2.23E+2 calls took 4.06E-2; 6.7% To CLOSE-INPUT-CHANNEL 2.23E+2 calls took 2.61E-2; 4.3% To self/unprofiled functions 9.56E-4; 0.2% From TRANS-EVAL-NO-WARNING 2.04E+2 calls took 5.90E-1; 96.9% From CHK-RAISE-PORTCULLIS2 1.80E+1 calls took 1.57E-2; 2.6% From other functions 1.00E+0 calls took 3.31E-3; 0.5%) (CHK-EMBEDDED-EVENT-FORM Calls 3.00E+4 Time of all outermost calls 0.61 Time per call 2.03E-5 Heap bytes allocated 1.50E+7; 0.1% Heap bytes allocated per call 500.65 To MACROEXPAND1 6.28E+3 calls took 5.66E-1; 93.2% To self/unprofiled functions 3.31E-2; 5.5% To TRUE-LISTP 6.75E+4 calls took 6.16E-3; 1.0% To other functions 1.63E+4 calls took 1.94E-3; 0.3% From TRANS-EVAL-NO-WARNING 5.67E+3 calls took 2.72E-1; 44.8% From PROGN-FN1 1.10E+4 calls took 2.36E-1; 38.9% From ENCAPSULATE-PASS-2 1.29E+4 calls took 9.48E-2; 15.6% From other functions 3.33E+2 calls took 4.03E-3; 0.7%) (TRANSLATE Calls 3.96E+4 Time of all outermost calls 0.60 Time per call 1.52E-5 Heap bytes allocated 2.05E+7; 0.2% Heap bytes allocated per call 518.36 To TRANSLATE-CMP 3.96E+4 calls took 5.80E-1; 96.3% To self/unprofiled functions 2.24E-2; 3.7% From DEFTHM-FN1 4.94E+3 calls took 2.07E-1; 34.3% From SIMPLE-TRANSLATE-AND-EVAL 1.30E+4 calls took 1.65E-1; 27.4% From PROGN-FN1 6.72E+3 calls took 1.07E-1; 17.8% From ENCAPSULATE-PASS-2 4.00E+3 calls took 5.83E-2; 9.7% From TRANSLATE-TERM-LST 5.65E+3 calls took 2.92E-2; 4.8% From TRANS-EVAL-NO-WARNING 1.19E+3 calls took 1.48E-2; 2.4% From TRANSLATE-MEASURES 2.81E+3 calls took 1.15E-2; 1.9% From other functions 1.27E+3 calls took 9.58E-3; 1.6%) (DISTRIBUTE-FIRST-IF Calls 2.68E+5 Time of all outermost calls 0.58 Time per call 2.16E-6 Heap bytes allocated 6.88E+6; 0.1% Heap bytes allocated per call 25.66 To NORMALIZE-WITH-TYPE-SET 2.23E+5 calls took 4.23E-1; 73.1% To self/unprofiled functions 4.56E-2; 7.9% To NORMALIZE-LST 9.92E+3 calls took 4.39E-2; 7.6% To NOT-IDENT 8.45E+3 calls took 2.27E-2; 3.9% To ASSUME-TRUE-FALSE-BC 1.64E+3 calls took 1.27E-2; 2.2% To FIRST-IF 2.34E+5 calls took 1.15E-2; 2.0% To other functions 5.88E+4 calls took 1.11E-2; 1.9% To SUBCOR-VAR 1.17E+4 calls took 8.23E-3; 1.4% From NORMALIZE 4.78E+4 calls took 2.93E-1; 50.6% From NORMALIZE-LST 2.10E+5 calls took 2.85E-1; 49.4%) (TRANSLATE11-CALL-1 Calls 1.32E+5 Time of all outermost calls 0.58 Time per call 4.38E-6 Heap bytes allocated 2.25E+7; 0.2% Heap bytes allocated per call 171.04 To TRANSLATE11-LST 8.15E+4 calls took 3.15E-1; 54.7% To MACROEXPAND1-CMP 8.25E+3 calls took 7.50E-2; 13.0% To self/unprofiled functions 7.19E-2; 12.5% To TRANSLATE11-LET 1.06E+3 calls took 3.67E-2; 6.4% To ILKS-PER-ARGUMENT-SLOT 8.07E+4 calls took 2.33E-2; 4.0% To other functions 4.15E+5 calls took 2.06E-2; 3.6% To FGETPROP 1.09E+5 calls took 1.29E-2; 2.2% To STOBJS-IN-OUT 2.99E+4 calls took 7.36E-3; 1.3% To TRANSLATE11-VAR-OR-QUOTE-EXIT 5.13E+4 calls took 6.84E-3; 1.2% To LEGAL-VARIABLE-OR-CONSTANT-NAMEP 5.13E+4 calls took 6.19E-3; 1.1% From TRANSLATE11-CALL 4.86E+4 calls took 4.67E-1; 81.1% From TRANSLATE11-LST 4.67E+4 calls took 1.08E-1; 18.7% From other functions 3.62E+4 calls took 9.80E-4; ?%) (MACROEXPAND1 Calls 6.28E+3 Time of all outermost calls 0.57 Time per call 9.01E-5 Heap bytes allocated 1.35E+7; 0.1% Heap bytes allocated per call 2.16E+3 To MACROEXPAND1-CMP 6.28E+3 calls took 5.60E-1; 98.9% To self/unprofiled functions 6.04E-3; 1.1% To other functions 6.28E+3 calls took 1.03E-4; 0.0% From CHK-EMBEDDED-EVENT-FORM 6.28E+3 calls took 5.66E-1; 100.0%) (TRANSLATE11-MV-LET Calls 3.57E+3 Time of all outermost calls 0.54 Time per call 1.51E-4 Heap bytes allocated 2.51E+7; 0.2% Heap bytes allocated per call 7.03E+3 To MACROEXPAND1-CMP 2.69E+4 calls took 1.93E-1; 35.9% To TRANSLATE11-LST 1.42E+4 calls took 1.28E-1; 23.7% To TRANSLATE11-CALL 5.43E+3 calls took 6.54E-2; 12.1% To self/unprofiled functions 4.99E-2; 9.3% To other functions 2.81E+5 calls took 4.35E-2; 8.1% To TRANSLATE11-LET 4.68E+3 calls took 1.53E-2; 2.8% To COLLECT-DECLARATIONS-CMP 8.12E+3 calls took 1.19E-2; 2.2% To ARGLISTP 8.12E+3 calls took 1.00E-2; 1.9% To FGETPROP 8.10E+4 calls took 9.27E-3; 1.7% To ALL-VARS 1.16E+4 calls took 6.38E-3; 1.2% To GENVAR 3.52E+3 calls took 6.13E-3; 1.1% From TRANSLATE11-LET 1.53E+3 calls took 4.79E-1; 88.9% From TRANSLATE11 4.96E+2 calls took 5.59E-2; 10.4% From other functions 1.54E+3 calls took 3.98E-3; 0.7%) (NORMALIZE-WITH-TYPE-SET Calls 3.73E+5 Time of all outermost calls 0.51 Time per call 1.37E-6 Heap bytes allocated 6.07E+6; 0.1% Heap bytes allocated per call 16.30 To TYPE-SET-BC 3.73E+5 calls took 4.80E-1; 93.9% To self/unprofiled functions 3.09E-2; 6.1% From DISTRIBUTE-FIRST-IF 2.23E+5 calls took 4.23E-1; 82.7% From NORMALIZE-LST 1.47E+5 calls took 8.39E-2; 16.4% From other functions 3.22E+3 calls took 4.49E-3; 0.9%) (TYPE-SET-BC Calls 3.73E+5 Time of all outermost calls 0.48 Time per call 1.29E-6 Heap bytes allocated 6.07E+6; 0.1% Heap bytes allocated per call 16.30 To TYPE-SET-REC 3.73E+5 calls took 4.54E-1; 94.5% To self/unprofiled functions 2.65E-2; 5.5% From NORMALIZE-WITH-TYPE-SET 3.73E+5 calls took 4.80E-1; 100.0% From other functions 5.10E+1 calls took 1.13E-4; ?%) (CHK-INPUT-OBJECT-FILE Calls 1.36E+3 Time of all outermost calls 0.47 Time per call 3.49E-4 Heap bytes allocated 2.23E+7; 0.2% Heap bytes allocated per call 1.64E+4 To OPEN-INPUT-OBJECT-FILE 1.36E+3 calls took 2.36E-1; 49.7% To self/unprofiled functions 1.75E-1; 37.0% To CLOSE-INPUT-CHANNEL 1.36E+3 calls took 6.05E-2; 12.8% To other functions 8.16E+3 calls took 2.44E-3; 0.5% From CHK-RAISE-PORTCULLIS2 7.33E+2 calls took 2.62E-1; 55.2% From TRANS-EVAL-NO-WARNING 6.26E+2 calls took 2.12E-1; 44.6% From other functions 1.00E+0 calls took 1.01E-3; 0.2%) (IN-THEORY-FN Calls 1.65E+3 Time of all outermost calls 0.47 Time per call 2.87E-4 Heap bytes allocated 2.28E+7; 0.2% Heap bytes allocated per call 1.38E+4 To INSTALL-EVENT 1.53E+3 calls took 1.42E-1; 30.0% To UPDATE-CURRENT-THEORY 1.53E+3 calls took 1.29E-1; 27.2% To TRANSLATE-IN-THEORY-HINT 1.53E+3 calls took 1.14E-1; 24.0% To self/unprofiled functions 3.86E-2; 8.2% To PRINT-SUMMARY 1.53E+3 calls took 2.11E-2; 4.5% To INITIALIZE-SUMMARY-ACCUMULATORS 1.53E+3 calls took 1.79E-2; 3.8% To other functions 2.78E+4 calls took 1.09E-2; 2.3% From ENCAPSULATE-PASS-2 9.11E+2 calls took 2.40E-1; 50.9% From TRANS-EVAL-NO-WARNING 1.46E+2 calls took 1.21E-1; 25.6% From PROGN-FN1 5.82E+2 calls took 1.10E-1; 23.2% From other functions 1.00E+1 calls took 1.55E-3; 0.3%) (NORMALIZE-LST Calls 2.76E+5 Time of all outermost calls 0.45 Time per call 1.64E-6 Heap bytes allocated 1.43E+7; 0.1% Heap bytes allocated per call 51.73 To DISTRIBUTE-FIRST-IF 2.10E+5 calls took 2.85E-1; 63.0% To NORMALIZE-WITH-TYPE-SET 1.47E+5 calls took 8.39E-2; 18.5% To self/unprofiled functions 5.12E-2; 11.3% To CONS-TERM 2.12E+5 calls took 2.28E-2; 5.0% To other functions 6.12E+5 calls took 1.02E-2; 2.2% From NORMALIZE 5.54E+4 calls took 4.10E-1; 90.3% From DISTRIBUTE-FIRST-IF 9.92E+3 calls took 4.39E-2; 9.7% From other functions 2.11E+5 calls took 1.00E-4; ?%) (READ-OBJECT-FILE1 Calls 223 Time of all outermost calls 0.44 Time per call 1.98E-3 Heap bytes allocated 1.08E+7; 0.1% Heap bytes allocated per call 4.84E+4 To READ-OBJECT 6.09E+3 calls took 4.40E-1; 99.8% To self/unprofiled functions 1.02E-3; 0.2% From READ-OBJECT-FILE 2.23E+2 calls took 4.41E-1; 100.0%) (OPEN-INPUT-CHANNEL Calls 2.03E+3 Time of all outermost calls 0.43 Time per call 2.11E-4 Heap bytes allocated 1.69E+7; 0.2% Heap bytes allocated per call 8.34E+3 To self/unprofiled functions 4.02E-1; 94.2% To MAKE-INPUT-CHANNEL 2.03E+3 calls took 2.41E-2; 5.6% To other functions 4.06E+3 calls took 6.12E-4; 0.1% From OPEN-INPUT-OBJECT-FILE 1.58E+3 calls took 2.75E-1; 64.4% From CERTIFICATE-FILE-AND-INPUT-CHANNEL1 4.46E+2 calls took 1.52E-1; 35.6%) (PUT-INDUCTION-INFO Calls 1.83E+3 Time of all outermost calls 0.41 Time per call 2.24E-4 Heap bytes allocated 2.20E+7; 0.2% Heap bytes allocated per call 1.21E+4 To PROVE-TERMINATION-RECURSIVE 7.96E+2 calls took 2.98E-1; 72.7% To PUT-INDUCTION-INFO-RECURSIVE 7.96E+2 calls took 4.62E-2; 11.3% To TERMINATION-MACHINES 7.96E+2 calls took 2.57E-2; 6.3% To PROVE-TERMINATION-NON-RECURSIVE 1.03E+3 calls took 1.77E-2; 4.3% To SET-W 7.96E+2 calls took 1.58E-2; 3.9% To other functions 3.60E+3 calls took 3.84E-3; 0.9% To self/unprofiled functions 2.36E-3; 0.6% From DEFUNS-FN0 1.83E+3 calls took 4.10E-1; 100.0%) (SIMPLE-TRANSLATE-AND-EVAL Calls 1.30E+4 Time of all outermost calls 0.40 Time per call 3.11E-5 Heap bytes allocated 2.11E+7; 0.2% Heap bytes allocated per call 1.62E+3 To TRANSLATE 1.30E+4 calls took 1.65E-1; 40.9% To EV-REC-LST 3.69E+3 calls took 1.33E-1; 32.8% To SET-DIFFERENCE-CURRENT-THEORY-FN 1.47E+3 calls took 4.80E-2; 11.9% To self/unprofiled functions 2.73E-2; 6.8% To other functions 1.40E+5 calls took 1.59E-2; 3.9% To XDOC::XDOC-PREPEND-FN 2.13E+2 calls took 6.63E-3; 1.6% To ALL-VARS 1.30E+4 calls took 4.33E-3; 1.1% To UNION-THEORIES-FN 3.00E+0 calls took 4.31E-3; 1.1% From TABLE-FN 1.14E+4 calls took 1.68E-1; 41.5% From EVAL-THEORY-EXPR 1.53E+3 calls took 1.50E-1; 37.2% From CHK-ACCEPTABLE-DEFPKG 2.80E+1 calls took 7.54E-2; 18.6% From DEFCONST-VAL 3.50E+1 calls took 1.03E-2; 2.5% From other functions 1.50E+1 calls took 3.75E-4; ?%) (EXTEND-PATHNAME Calls 2.67E+4 Time of all outermost calls 0.39 Time per call 1.47E-5 Heap bytes allocated 2.76E+7; 0.2% Heap bytes allocated per call 1.03E+3 To self/unprofiled functions 3.51E-1; 89.0% To OUR-MERGE-PATHNAMES 2.67E+4 calls took 2.71E-2; 6.9% To other functions 9.11E+4 calls took 8.63E-3; 2.2% To OS 3.22E+4 calls took 7.70E-3; 2.0% From PARSE-BOOK-NAME 2.72E+3 calls took 3.64E-1; 92.4% From SYSFILE-TO-FILENAME 2.40E+4 calls took 2.99E-2; 7.6%) (PARSE-BOOK-NAME Calls 2.72E+3 Time of all outermost calls 0.38 Time per call 1.41E-4 Heap bytes allocated 2.22E+7; 0.2% Heap bytes allocated per call 8.16E+3 To EXTEND-PATHNAME 2.72E+3 calls took 3.64E-1; 95.0% To self/unprofiled functions 1.39E-2; 3.6% To FIRST-N-AC 2.72E+3 calls took 5.48E-3; 1.4% From INCLUDE-BOOK-FN 1.36E+3 calls took 1.96E-1; 51.1% From CHK-RAISE-PORTCULLIS2 7.33E+2 calls took 1.05E-1; 27.3% From TRANS-EVAL-NO-WARNING 6.26E+2 calls took 8.28E-2; 21.6%) (READ-FILE-INTO-TEMPLATE Calls 223 Time of all outermost calls 0.35 Time per call 1.56E-3 Heap bytes allocated 4.47E+7; 0.4% Heap bytes allocated per call 2.00E+5 To READ-OBJECT 1.66E+3 calls took 3.47E-1; 99.7% To self/unprofiled functions 7.95E-4; 0.2% To other functions 2.83E+2 calls took 1.45E-4; 0.0% From CHK-RAISE-PORTCULLIS 2.01E+2 calls took 3.41E-1; 98.1% From TRANS-EVAL-NO-WARNING 4.00E+0 calls took 4.66E-3; 1.3% From other functions 1.80E+1 calls took 2.09E-3; 0.6%) (PRINT-SUMMARY Calls 2.41E+4 Time of all outermost calls 0.34 Time per call 1.39E-5 Heap bytes allocated 1.73E+7; 0.2% Heap bytes allocated per call 717.49 To INCREMENT-TIMER 2.41E+4 calls took 1.27E-1; 37.6% To POP-TIMER 9.65E+4 calls took 6.22E-2; 18.5% To PRINT-REDEFINITION-WARNING 2.22E+4 calls took 5.94E-2; 17.6% To self/unprofiled functions 5.09E-2; 15.1% To PUT-EVENT-DATA 9.46E+4 calls took 1.43E-2; 4.3% To other functions 9.46E+4 calls took 9.03E-3; 2.7% To POP-WARNING-FRAME 2.41E+4 calls took 4.96E-3; 1.5% To PROVER-STEPS 2.41E+4 calls took 4.63E-3; 1.4% To GET-TIMER 9.65E+4 calls took 4.50E-3; 1.3% From TABLE-FN1 5.55E+3 calls took 7.63E-2; 22.7% From DEFTHM-FN1 4.94E+3 calls took 6.96E-2; 20.7% From DEFUNS-FN 2.70E+3 calls took 4.88E-2; 14.5% From PROGN-FN1 3.69E+3 calls took 4.54E-2; 13.5% From IN-THEORY-FN 1.53E+3 calls took 2.11E-2; 6.3% From ENCAPSULATE-PASS-2 1.58E+3 calls took 1.88E-2; 5.6% From DEFMACRO-FN 1.18E+3 calls took 1.66E-2; 4.9% From ENCAPSULATE-FN 1.20E+3 calls took 1.46E-2; 4.3% From CHK-RAISE-PORTCULLIS2 7.33E+2 calls took 1.16E-2; 3.4% From TRANS-EVAL-NO-WARNING 6.26E+2 calls took 7.72E-3; 2.3% From other functions 4.08E+2 calls took 5.82E-3; 1.7%) (TAU-VISIT-EVENT Calls 1.75E+4 Time of all outermost calls 0.32 Time per call 1.83E-5 Heap bytes allocated 4.44E+6; 0.0% Heap bytes allocated per call 254.14 To TAU-VISIT-DEFUN 2.56E+3 calls took 1.74E-1; 54.5% To TAU-VISIT-DEFTHM 4.86E+3 calls took 1.23E-1; 38.3% To TAU-VISIT-DEFUNS 1.04E+2 calls took 1.74E-2; 5.4% To self/unprofiled functions 5.71E-3; 1.8% From INSTALL-EVENT 1.75E+4 calls took 3.20E-1; 100.0%) (INSTALL-EVENT-DEFUNS Calls 2.67E+3 Time of all outermost calls 0.30 Time per call 1.14E-4 Heap bytes allocated 9.57E+6; 0.1% Heap bytes allocated per call 3.59E+3 To INSTALL-EVENT 2.67E+3 calls took 2.99E-1; 98.5% To other functions 5.54E+3 calls took 2.34E-3; 0.8% To self/unprofiled functions 2.33E-3; 0.8% From DEFUNS-FN 2.67E+3 calls took 3.04E-1; 100.0%) (INITIALIZE-SUMMARY-ACCUMULATORS Calls 2.41E+4 Time of all outermost calls 0.30 Time per call 1.25E-5 Heap bytes allocated 2.16E+7; 0.2% Heap bytes allocated per call 895.99 To INCREMENT-TIMER 2.41E+4 calls took 1.09E-1; 36.1% To TIME-TRACKER-FN 4.83E+4 calls took 1.02E-1; 33.8% To self/unprofiled functions 4.81E-2; 16.0% To PUSH-TIMER 9.65E+4 calls took 3.50E-2; 11.6% To PUSH-WARNING-FRAME 2.41E+4 calls took 3.85E-3; 1.3% To GET-TIMER 2.41E+4 calls took 3.73E-3; 1.2% To other functions 1.00E+0 calls took 9.30E-6; <0.01% From TABLE-FN1 5.55E+3 calls took 6.72E-2; 22.3% From DEFTHM-FN1 4.94E+3 calls took 6.33E-2; 21.0% From PROGN-FN1 3.69E+3 calls took 4.47E-2; 14.8% From DEFUNS-FN 2.70E+3 calls took 3.16E-2; 10.5% From ENCAPSULATE-PASS-2 1.58E+3 calls took 1.86E-2; 6.2% From IN-THEORY-FN 1.53E+3 calls took 1.79E-2; 5.9% From CHK-RAISE-PORTCULLIS2 7.33E+2 calls took 1.51E-2; 5.0% From ENCAPSULATE-FN 1.20E+3 calls took 1.44E-2; 4.8% From DEFMACRO-FN 1.18E+3 calls took 1.40E-2; 4.6% From TRANS-EVAL-NO-WARNING 6.26E+2 calls took 8.40E-3; 2.8% From other functions 4.08E+2 calls took 5.78E-3; 1.9%) (PROVE-TERMINATION-RECURSIVE Calls 796 Time of all outermost calls 0.30 Time per call 3.74E-4 Heap bytes allocated 1.43E+7; 0.1% Heap bytes allocated per call 1.80E+4 To TRANSLATE-HINTS 7.39E+2 calls took 2.79E-1; 93.7% To PROVE-TERMINATION 7.96E+2 calls took 1.38E-2; 4.6% To GUESS-MEASURE-ALIST 7.96E+2 calls took 3.34E-3; 1.1% To self/unprofiled functions 1.21E-3; 0.4% To other functions 7.96E+2 calls took 3.68E-4; 0.1% From PUT-INDUCTION-INFO 7.96E+2 calls took 2.98E-1; 100.0%) (TRANSLATE-HINTS Calls 739 Time of all outermost calls 0.28 Time per call 3.78E-4 Heap bytes allocated 1.39E+7; 0.1% Heap bytes allocated per call 1.87E+4 To TRANSLATE-HINTS2 7.39E+2 calls took 2.78E-1; 99.7% To self/unprofiled functions 6.99E-4; 0.3% To other functions 7.39E+2 calls took 2.66E-4; 0.1% From PROVE-TERMINATION-RECURSIVE 7.39E+2 calls took 2.79E-1; 100.0%) (TRANSLATE-HINTS2 Calls 739 Time of all outermost calls 0.28 Time per call 3.76E-4 Heap bytes allocated 1.39E+7; 0.1% Heap bytes allocated per call 1.87E+4 To TRANSLATE-HINTS1 7.39E+2 calls took 2.76E-1; 99.1% To other functions 1.48E+3 calls took 1.85E-3; 0.7% To self/unprofiled functions 7.59E-4; 0.3% From TRANSLATE-HINTS 7.39E+2 calls took 2.78E-1; 100.0%) (OPEN-INPUT-OBJECT-FILE Calls 1.58E+3 Time of all outermost calls 0.28 Time per call 1.75E-4 Heap bytes allocated 1.32E+7; 0.1% Heap bytes allocated per call 8.32E+3 To OPEN-INPUT-CHANNEL 1.58E+3 calls took 2.75E-1; 99.5% To self/unprofiled functions 1.26E-3; 0.5% From CHK-INPUT-OBJECT-FILE 1.36E+3 calls took 2.36E-1; 85.3% From READ-OBJECT-FILE 2.23E+2 calls took 4.06E-2; 14.7%) (TRANSLATE-HINTS1 Calls 739 Time of all outermost calls 0.28 Time per call 3.73E-4 Heap bytes allocated 1.39E+7; 0.1% Heap bytes allocated per call 1.87E+4 To TRANSLATE-HINT-EXPRESSION 2.69E+3 calls took 2.74E-1; 99.6% To self/unprofiled functions 1.11E-3; 0.4% From TRANSLATE-HINTS2 7.39E+2 calls took 2.76E-1; 100.0%) (TRANSLATE-HINT-EXPRESSION Calls 2.69E+3 Time of all outermost calls 0.27 Time per call 1.02E-4 Heap bytes allocated 1.38E+7; 0.1% Heap bytes allocated per call 5.13E+3 To TRANSLATE-SIMPLE-OR-ERROR-TRIPLE 2.69E+3 calls took 2.69E-1; 97.9% To ALL-VARS 2.69E+3 calls took 2.91E-3; 1.1% To self/unprofiled functions 2.86E-3; 1.0% From TRANSLATE-HINTS1 2.69E+3 calls took 2.74E-1; 100.0%) (TYPE-SET-WITH-RULES Calls 1.74E+5 Time of all outermost calls 0.27 Time per call 1.56E-6 Heap bytes allocated 2.95E+6; 0.0% Heap bytes allocated per call 16.91 To TYPE-SET-PRIMITIVE 1.42E+5 calls took 1.28E-1; 47.2% To TYPE-SET-WITH-RULE 2.86E+5 calls took 1.12E-1; 41.2% To self/unprofiled functions 3.15E-2; 11.6% From TYPE-SET-REC 1.42E+5 calls took 2.72E-1; 99.8% From other functions 3.24E+4 calls took 4.66E-4; ?%) (TRANSLATE-SIMPLE-OR-ERROR-TRIPLE Calls 2.69E+3 Time of all outermost calls 0.27 Time per call 9.98E-5 Heap bytes allocated 1.34E+7; 0.1% Heap bytes allocated per call 4.98E+3 To TRANSLATE1 2.69E+3 calls took 2.66E-1; 99.1% To self/unprofiled functions 1.52E-3; 0.6% To other functions 5.38E+3 calls took 8.60E-4; 0.3% From TRANSLATE-HINT-EXPRESSION 2.69E+3 calls took 2.69E-1; 100.0%) (ASSUME-TRUE-FALSE-BC Calls 5.24E+4 Time of all outermost calls 0.27 Time per call 5.11E-6 Heap bytes allocated 6.94E+6; 0.1% Heap bytes allocated per call 132.33 To ASSUME-TRUE-FALSE-REC 5.24E+4 calls took 2.52E-1; 94.1% To self/unprofiled functions 1.29E-2; 4.8% To CONSTANT-NIL-FUNCTION-ARITY-0 5.24E+4 calls took 2.87E-3; 1.1% From NORMALIZE 4.96E+4 calls took 2.50E-1; 93.3% From DISTRIBUTE-FIRST-IF 1.64E+3 calls took 1.27E-2; 4.7% From NORMALIZE-LST 9.68E+2 calls took 4.18E-3; 1.6% From other functions 1.89E+2 calls took 9.92E-4; ?%) (ASSUME-TRUE-FALSE-REC Calls 9.17E+4 Time of all outermost calls 0.26 Time per call 2.79E-6 Heap bytes allocated 7.05E+6; 0.1% Heap bytes allocated per call 76.85 To ASSUME-TRUE-FALSE-IF 2.37E+3 calls took 1.04E-1; 40.6% To TYPE-SET-REC 3.44E+4 calls took 3.91E-2; 15.3% To self/unprofiled functions 2.80E-2; 11.0% To EXTEND-WITH-PROPER/IMPROPER-CONS-TS-TUPLE 3.49E+4 calls took 1.99E-2; 7.8% To ASSUME-TRUE-FALSE1 3.52E+3 calls took 1.79E-2; 7.0% To TERM-ORDER 1.19E+4 calls took 1.18E-2; 4.6% To CANONICAL-REPRESENTATIVE 2.38E+4 calls took 6.81E-3; 2.7% To MOST-RECENT-ENABLED-RECOG-TUPLE 2.67E+4 calls took 6.76E-3; 2.6% To MV-ATF 4.75E+4 calls took 5.80E-3; 2.3% To EXTEND-TYPE-ALIST1 2.38E+4 calls took 5.07E-3; 2.0% To ASSOC-EQUIV 1.19E+4 calls took 3.85E-3; 1.5% To GLOBAL-VAL 2.67E+4 calls took 3.67E-3; 1.4% To other functions 4.02E+4 calls took 3.15E-3; 1.2% From ASSUME-TRUE-FALSE-BC 5.24E+4 calls took 2.52E-1; 98.7% From other functions 3.92E+4 calls took 3.22E-3; 1.3%) (INCREMENT-TIMER Calls 5.19E+4 Time of all outermost calls 0.25 Time per call 4.85E-6 Heap bytes allocated 9.91E+6; 0.1% Heap bytes allocated per call 190.87 To MAIN-TIMER 5.19E+4 calls took 1.74E-1; 69.1% To self/unprofiled functions 4.66E-2; 18.5% To SET-TIMER 5.19E+4 calls took 2.64E-2; 10.5% To GET-TIMER 5.19E+4 calls took 4.89E-3; 1.9% From PRINT-SUMMARY 2.41E+4 calls took 1.27E-1; 50.2% From INITIALIZE-SUMMARY-ACCUMULATORS 2.41E+4 calls took 1.09E-1; 43.1% From PROVE-TERMINATION 3.65E+3 calls took 1.67E-2; 6.6%) (CHK-IN-PACKAGE Calls 446 Time of all outermost calls 0.24 Time per call 5.28E-4 Heap bytes allocated 1.42E+5; 0.0% Heap bytes allocated per call 317.38 To READ-OBJECT 4.46E+2 calls took 2.28E-1; 96.9% To ASSOC-EQUAL 4.46E+2 calls took 3.87E-3; 1.6% To self/unprofiled functions 1.76E-3; 0.7% To other functions 8.92E+2 calls took 1.60E-3; 0.7% From CHK-CERTIFICATE-FILE 2.01E+2 calls took 1.26E-1; 53.6% From READ-OBJECT-FILE 2.23E+2 calls took 1.01E-1; 42.8% From CHK-RAISE-PORTCULLIS2 1.80E+1 calls took 6.54E-3; 2.8% From other functions 4.00E+0 calls took 1.89E-3; 0.8%) (BIND-MACRO-ARGS Calls 1.69E+5 Time of all outermost calls 0.22 Time per call 1.29E-6 Heap bytes allocated 1.24E+7; 0.1% Heap bytes allocated per call 73.68 To BIND-MACRO-ARGS1 1.69E+5 calls took 1.83E-1; 84.0% To self/unprofiled functions 3.49E-2; 16.0% From MACROEXPAND1-CMP 1.69E+5 calls took 2.18E-1; 100.0%) (ASSOC-TYPE-ALIST Calls 7.04E+5 Time of all outermost calls 0.21 Time per call 2.94E-7 Heap bytes allocated 2.39E+5; 0.0% Heap bytes allocated per call 0.34 To ASSOC-EQUAL 4.45E+5 calls took 9.29E-2; 44.8% To self/unprofiled functions 5.96E-2; 28.7% To FGETPROP 4.44E+5 calls took 2.99E-2; 14.4% To ASSOC-EQUIV+ 1.93E+4 calls took 2.48E-2; 12.0% From TYPE-SET-REC 5.42E+5 calls took 1.69E-1; 81.5% From TYPE-SET-PRIMITIVE 1.44E+5 calls took 3.28E-2; 15.8% From LOOK-IN-TYPE-ALIST 1.28E+4 calls took 4.84E-3; 2.3% From other functions 5.41E+3 calls took 7.24E-4; ?%) (DEFPKG-FN Calls 28 Time of all outermost calls 0.20 Time per call 7.21E-3 Heap bytes allocated 2.65E+7; 0.2% Heap bytes allocated per call 9.48E+5 To CHK-ACCEPTABLE-DEFPKG 2.80E+1 calls took 1.52E-1; 75.4% To INSTALL-EVENT 2.80E+1 calls took 4.72E-2; 23.4% To other functions 5.32E+2 calls took 2.11E-3; 1.0% To self/unprofiled functions 2.66E-4; 0.1% From CHK-RAISE-PORTCULLIS2 2.80E+1 calls took 2.02E-1; 100.0%) (DEFMACRO-FN Calls 1.18E+3 Time of all outermost calls 0.20 Time per call 1.67E-4 Heap bytes allocated 8.11E+6; 0.1% Heap bytes allocated per call 6.86E+3 To INSTALL-EVENT 1.16E+3 calls took 4.10E-2; 20.8% To TRANSLATE-CMP 1.18E+3 calls took 3.84E-2; 19.5% To ANCESTRAL-LAMBDA$S-BY-CALLER 2.36E+3 calls took 3.44E-2; 17.4% To PRINT-SUMMARY 1.18E+3 calls took 1.66E-2; 8.4% To INITIALIZE-SUMMARY-ACCUMULATORS 1.18E+3 calls took 1.40E-2; 7.1% To self/unprofiled functions 1.02E-2; 5.2% To other functions 2.71E+4 calls took 9.89E-3; 5.0% To CHK-FREE-AND-IGNORED-VARS 1.16E+3 calls took 8.21E-3; 4.2% To CHK-MACRO-ARGLIST 1.18E+3 calls took 8.04E-3; 4.1% To TRANSLATE 1.18E+3 calls took 5.96E-3; 3.0% To COLLECT-NON-APPLY$-PRIMPS 2.36E+3 calls took 4.55E-3; 2.3% To CHK-JUST-NEW-NAME 1.16E+3 calls took 3.02E-3; 1.5% To COLLECT-DECLARATIONS 1.18E+3 calls took 2.79E-3; 1.4% From ENCAPSULATE-PASS-2 5.45E+2 calls took 8.89E-2; 45.1% From TRANS-EVAL-NO-WARNING 3.33E+2 calls took 6.45E-2; 32.7% From PROGN-FN1 3.00E+2 calls took 4.32E-2; 21.9% From other functions 3.00E+0 calls took 5.08E-4; ?%) (TAU-VISIT-DEFUNS Calls 2.67E+3 Time of all outermost calls 0.19 Time per call 7.16E-5 Heap bytes allocated 1.72E+6; 0.0% Heap bytes allocated per call 645.82 To TAU-VISIT-DEFUNS1 2.67E+3 calls took 1.66E-1; 87.0% To DISCOVER-TAU-PREDS 2.67E+3 calls took 2.32E-2; 12.2% To self/unprofiled functions 1.68E-3; 0.9% From TAU-VISIT-DEFUN 2.56E+3 calls took 1.73E-1; 90.9% From TAU-VISIT-EVENT 1.04E+2 calls took 1.74E-2; 9.1%) (ADD-RULES Calls 4.89E+3 Time of all outermost calls 0.18 Time per call 3.75E-5 Heap bytes allocated 6.61E+6; 0.1% Heap bytes allocated per call 1.35E+3 To ADD-RULES1 4.89E+3 calls took 1.68E-1; 91.6% To self/unprofiled functions 5.23E-3; 2.9% To MAKE-RUNES 4.89E+3 calls took 2.88E-3; 1.6% To PUTPROP 1.95E+4 calls took 2.78E-3; 1.5% To other functions 9.77E+3 calls took 2.33E-3; 1.3% To TRUNCATE-CLASSES 4.89E+3 calls took 2.19E-3; 1.2% From DEFTHM-FN1 4.86E+3 calls took 1.82E-1; 99.5% From other functions 2.80E+1 calls took 9.74E-4; ?%) (BIND-MACRO-ARGS1 Calls 1.69E+5 Time of all outermost calls 0.18 Time per call 1.08E-6 Heap bytes allocated 1.17E+7; 0.1% Heap bytes allocated per call 69.68 To BIND-MACRO-ARGS-KEYS 2.07E+4 calls took 9.89E-2; 54.1% To self/unprofiled functions 7.27E-2; 39.8% To BIND-MACRO-ARGS-AFTER-REST 8.90E+4 calls took 1.07E-2; 5.9% To other functions 1.13E+3 calls took 4.79E-4; 0.3% From BIND-MACRO-ARGS 1.69E+5 calls took 1.83E-1; 100.0%) (ADD-TAU-RULE1 Calls 6.19E+3 Time of all outermost calls 0.18 Time per call 2.88E-5 Heap bytes allocated 1.16E+6; 0.0% Heap bytes allocated per call 187.68 To ADD-TAU-SIGNATURE-RULE 2.56E+3 calls took 1.34E-1; 75.1% To ACCEPTABLE-TAU-RULEP 7.02E+3 calls took 2.54E-2; 14.3% To ADD-TAU-SIMPLE-RULE 5.80E+1 calls took 1.33E-2; 7.5% To self/unprofiled functions 4.26E-3; 2.4% To other functions 1.70E+1 calls took 1.27E-3; 0.7% From TAU-RULES-FROM-TYPE-PRESCRIPTIONS 1.31E+3 calls took 9.68E-2; 54.3% From ADD-TAU-RULE 4.88E+3 calls took 8.15E-2; 45.7%) NIL ACL2 !>Bye. ~/acl2/acl2$ alias make-acl2 alias make-acl2='mv make.log make-old.log ; (time nice make LISP=ccl) >& make.log&' ~/acl2/acl2$ alias lt alias lt='ls -lrt' ~/acl2/acl2$ lt total 932344 -rw-r--r-- 1 kaufmann staff 1500 Sep 7 02:18 Makefile lrwxr-xr-x 1 kaufmann staff 15 Sep 7 02:18 README.md -> books/README.md -rw-r--r-- 1 kaufmann staff 256 Sep 7 02:18 acl2-characters drwxr-xr-x 11 kaufmann staff 352 Sep 7 02:18 acl2-customization-files -rw-r--r-- 1 kaufmann staff 3583 Sep 7 02:18 all-files.txt -rw-r--r-- 1 kaufmann staff 3342 Sep 7 02:18 build-allegro-exe.cl drwxr-xr-x 55 kaufmann staff 1760 Sep 7 02:18 graphics -rw-r--r-- 1 kaufmann staff 5355 Sep 7 02:18 mcl-acl2-startup.lisp -rw-r--r-- 1 kaufmann staff 8065 Sep 7 02:18 workshops.html -rw-r--r-- 1 kaufmann staff 398 Sep 11 19:45 tmp.msg.~1~ -rw-r--r-- 1 kaufmann staff 1066 Sep 11 20:20 tmp.msg.~2~ -rw-r--r-- 1 kaufmann staff 35403 Oct 3 22:36 GNUmakefile -rw-r--r-- 1 kaufmann staff 2084 Oct 3 22:36 LICENSE -rw-r--r-- 1 kaufmann staff 16875 Oct 3 22:36 acl2-check.lisp -rw-r--r-- 1 kaufmann staff 92948 Oct 3 22:36 acl2-fns.lisp -rw-r--r-- 1 kaufmann staff 101851 Oct 3 22:36 acl2-init.lisp -rw-r--r-- 1 kaufmann staff 109745 Oct 3 22:36 acl2.lisp -rw-r--r-- 1 kaufmann staff 8587 Oct 3 22:36 akcl-acl2-trace.lisp -rw-r--r-- 1 kaufmann staff 10715 Oct 3 22:36 allegro-acl2-trace.lisp -rw-r--r-- 1 kaufmann staff 13504 Oct 3 22:36 apply-constraints.lisp -rw-r--r-- 1 kaufmann staff 169975 Oct 3 22:36 basis-b.lisp -rw-r--r-- 1 kaufmann staff 134211 Oct 3 22:36 bdd.lisp -rw-r--r-- 1 kaufmann staff 48467 Oct 3 22:36 boot-strap-pass-2-a.lisp -rw-r--r-- 1 kaufmann staff 31774 Oct 3 22:36 boot-strap-pass-2-b.lisp -rw-r--r-- 1 kaufmann staff 59443 Oct 3 22:36 futures-raw.lisp -rw-r--r-- 1 kaufmann staff 177251 Oct 3 22:36 hons-raw.lisp -rw-r--r-- 1 kaufmann staff 9881 Oct 3 22:36 hons.lisp -rw-r--r-- 1 kaufmann staff 151198 Oct 3 22:36 induct.lisp -rw-r--r-- 1 kaufmann staff 4118 Oct 3 22:36 init.lisp drwxr-xr-x 11 kaufmann staff 352 Oct 3 22:36 installation -rw-r--r-- 1 kaufmann staff 210271 Oct 3 22:36 ld.lisp -rw-r--r-- 1 kaufmann staff 153046 Oct 3 22:36 linear-a.lisp -rw-r--r-- 1 kaufmann staff 41811 Oct 3 22:36 linear-b.lisp -rw-r--r-- 1 kaufmann staff 214661 Oct 3 22:36 memoize-raw.lisp -rw-r--r-- 1 kaufmann staff 16097 Oct 3 22:36 memoize.lisp -rw-r--r-- 1 kaufmann staff 43865 Oct 3 22:36 multi-threading-raw.lisp -rw-r--r-- 1 kaufmann staff 2160 Oct 3 22:36 new.html -rw-r--r-- 1 kaufmann staff 41825 Oct 3 22:36 non-linear.lisp -rw-r--r-- 1 kaufmann staff 9243 Oct 3 22:36 openmcl-acl2-trace.lisp -rw-r--r-- 1 kaufmann staff 107642 Oct 3 22:36 other-processes.lisp -rw-r--r-- 1 kaufmann staff 5288 Oct 3 22:36 other-releases.html -rw-r--r-- 1 kaufmann staff 61416 Oct 3 22:36 parallel-raw.lisp -rw-r--r-- 1 kaufmann staff 41611 Oct 3 22:36 parallel.lisp -rw-r--r-- 1 kaufmann staff 65079 Oct 3 22:36 proof-builder-a.lisp -rw-r--r-- 1 kaufmann staff 1087 Oct 3 22:36 proof-builder-pkg.lisp -rw-r--r-- 1 kaufmann staff 425758 Oct 3 22:36 prove.lisp -rw-r--r-- 1 kaufmann staff 810498 Oct 3 22:36 rewrite.lisp -rw-r--r-- 1 kaufmann staff 13633 Oct 3 22:36 save-gprof.lsp -rw-r--r-- 1 kaufmann staff 68494 Oct 3 22:36 serialize-raw.lisp -rw-r--r-- 1 kaufmann staff 4313 Oct 3 22:36 serialize.lisp -rw-r--r-- 1 kaufmann staff 41454 Oct 3 22:36 type-set-a.lisp -rw-r--r-- 1 kaufmann staff 558067 Oct 3 22:36 type-set-b.lisp -rw-r--r-- 1 kaufmann staff 5143585 Oct 13 09:47 doc.lisp.backup -rw-r--r-- 1 kaufmann staff 409 Oct 13 10:59 tmp.msg.~3~ -rw-r--r-- 1 kaufmann staff 212506 Oct 13 11:03 proof-builder-b.lisp drwxr-xr-x 6 kaufmann staff 192 Oct 14 18:46 emacs -rw-r--r-- 1 kaufmann staff 20681 Oct 25 22:08 serialize-raw.fn -rw-r--r-- 1 kaufmann staff 241008 Oct 25 22:08 axioms.fn -rw-r--r-- 1 kaufmann staff 2691 Oct 25 22:08 hons.fn -rw-r--r-- 1 kaufmann staff 40010 Oct 25 22:08 hons-raw.fn -rw-r--r-- 1 kaufmann staff 88439 Oct 25 22:08 basis-a.fn -rw-r--r-- 1 kaufmann staff 1431 Oct 25 22:08 memoize.fn -rw-r--r-- 1 kaufmann staff 1337 Oct 25 22:08 serialize.fn -rw-r--r-- 1 kaufmann staff 62047 Oct 25 22:08 basis-b.fn -rw-r--r-- 1 kaufmann staff 9179 Oct 25 22:09 parallel.fn -rw-r--r-- 1 kaufmann staff 52450 Oct 25 22:09 memoize-raw.fn -rw-r--r-- 1 kaufmann staff 113406 Oct 25 22:09 translate.fn -rw-r--r-- 1 kaufmann staff 5615 Oct 25 22:09 type-set-a.fn -rw-r--r-- 1 kaufmann staff 47049 Oct 25 22:09 linear-a.fn -rw-r--r-- 1 kaufmann staff 116275 Oct 25 22:09 type-set-b.fn -rw-r--r-- 1 kaufmann staff 5871 Oct 25 22:09 linear-b.fn -rw-r--r-- 1 kaufmann staff 8983 Oct 25 22:09 non-linear.fn -rw-r--r-- 1 kaufmann staff 99047 Oct 25 22:09 tau.fn -rw-r--r-- 1 kaufmann staff 196824 Oct 25 22:09 rewrite.fn -rw-r--r-- 1 kaufmann staff 100035 Oct 25 22:09 simplify.fn -rw-r--r-- 1 kaufmann staff 43128 Oct 25 22:09 bdd.fn -rw-r--r-- 1 kaufmann staff 29131 Oct 25 22:09 other-processes.fn -rw-r--r-- 1 kaufmann staff 50929 Oct 25 22:09 induct.fn -rw-r--r-- 1 kaufmann staff 182 Oct 25 22:09 doc.fn -rw-r--r-- 1 kaufmann staff 231720 Oct 25 22:09 history-management.fn -rw-r--r-- 1 kaufmann staff 92704 Oct 25 22:09 prove.fn -rw-r--r-- 1 kaufmann staff 101019 Oct 25 22:09 defuns.fn -rw-r--r-- 1 kaufmann staff 40962 Oct 25 22:09 proof-builder-a.fn -rw-r--r-- 1 kaufmann staff 151230 Oct 25 22:09 defthm.fn -rw-r--r-- 1 kaufmann staff 351552 Oct 25 22:10 other-events.fn -rw-r--r-- 1 kaufmann staff 65860 Oct 25 22:10 ld.fn -rw-r--r-- 1 kaufmann staff 153434 Oct 25 22:10 proof-builder-b.fn -rw-r--r-- 1 kaufmann staff 8739 Oct 25 22:10 apply-raw.fn -rw-r--r-- 1 kaufmann staff 69664 Oct 25 22:10 interface-raw.fn -rw-r--r-- 1 kaufmann staff 4358 Oct 25 22:10 boot-strap-pass-2-a.fn -rw-r--r-- 1 kaufmann staff 3761 Oct 25 22:10 apply-prim.fn -rw-r--r-- 1 kaufmann staff 182 Oct 25 22:10 apply-constraints.fn -rw-r--r-- 1 kaufmann staff 628 Oct 25 22:10 apply.fn -rw-r--r-- 1 kaufmann staff 5271 Oct 25 22:10 boot-strap-pass-2-b.fn -rw-r--r-- 1 kaufmann staff 94203 Oct 25 22:10 serialize-raw.o -rw-r--r-- 1 kaufmann staff 943547 Oct 25 22:10 axioms.o -rw-r--r-- 1 kaufmann staff 11213 Oct 25 22:10 hons.o -rw-r--r-- 1 kaufmann staff 162427 Oct 25 22:10 hons-raw.o -rw-r--r-- 1 kaufmann staff 470334 Oct 25 22:10 basis-a.o -rw-r--r-- 1 kaufmann staff 25385 Oct 25 22:10 memoize.o -rw-r--r-- 1 kaufmann staff 8215 Oct 25 22:10 serialize.o -rw-r--r-- 1 kaufmann staff 259262 Oct 25 22:10 basis-b.o -rw-r--r-- 1 kaufmann staff 42756 Oct 25 22:10 parallel.o -rw-r--r-- 1 kaufmann staff 254365 Oct 25 22:10 memoize-raw.o -rw-r--r-- 1 kaufmann staff 578064 Oct 25 22:10 translate.o -rw-r--r-- 1 kaufmann staff 43950 Oct 25 22:10 type-set-a.o -rw-r--r-- 1 kaufmann staff 136257 Oct 25 22:10 linear-a.o -rw-r--r-- 1 kaufmann staff 459472 Oct 25 22:11 type-set-b.o -rw-r--r-- 1 kaufmann staff 42955 Oct 25 22:11 linear-b.o -rw-r--r-- 1 kaufmann staff 42594 Oct 25 22:11 non-linear.o -rw-r--r-- 1 kaufmann staff 372660 Oct 25 22:11 tau.o -rw-r--r-- 1 kaufmann staff 888438 Oct 25 22:11 rewrite.o -rw-r--r-- 1 kaufmann staff 388346 Oct 25 22:11 simplify.o -rw-r--r-- 1 kaufmann staff 205649 Oct 25 22:11 bdd.o -rw-r--r-- 1 kaufmann staff 126193 Oct 25 22:11 other-processes.o -rw-r--r-- 1 kaufmann staff 192767 Oct 25 22:11 induct.o -rw-r--r-- 1 kaufmann staff 5096021 Oct 25 22:11 doc.o -rw-r--r-- 1 kaufmann staff 1454328 Oct 25 22:11 history-management.o -rw-r--r-- 1 kaufmann staff 817348 Oct 25 22:11 prove.o -rw-r--r-- 1 kaufmann staff 514359 Oct 25 22:11 defuns.o -rw-r--r-- 1 kaufmann staff 225772 Oct 25 22:11 proof-builder-a.o -rw-r--r-- 1 kaufmann staff 811204 Oct 25 22:11 defthm.o -rw-r--r-- 1 kaufmann staff 2975921 Oct 25 22:12 other-events.o -rw-r--r-- 1 kaufmann staff 441777 Oct 25 22:12 ld.o -rw-r--r-- 1 kaufmann staff 723472 Oct 25 22:12 proof-builder-b.o -rw-r--r-- 1 kaufmann staff 51015 Oct 25 22:12 apply-raw.o -rw-r--r-- 1 kaufmann staff 495501 Oct 25 22:12 interface-raw.o -rw-r--r-- 1 kaufmann staff 25458 Oct 25 22:12 boot-strap-pass-2-a.o -rw-r--r-- 1 kaufmann staff 23146 Oct 25 22:12 apply-prim.o -rw-r--r-- 1 kaufmann staff 719 Oct 25 22:12 apply-constraints.o -rw-r--r-- 1 kaufmann staff 3132 Oct 25 22:12 apply.o -rw-r--r-- 1 kaufmann staff 33201 Oct 25 22:12 boot-strap-pass-2-b.o -rw-r--r-- 1 kaufmann staff 111731 Oct 25 22:12 acl2-fns.o -rwxrwxr-x 1 kaufmann staff 106 Oct 25 22:15 gcl-saved_acl2 -rwxr-xr-x 1 kaufmann staff 267894560 Oct 25 22:15 gcl-saved_acl2.gcl -rw-r--r-- 1 kaufmann staff 22214 Oct 30 07:13 apply-prim.lisp -rw-r--r-- 1 kaufmann staff 181655 Oct 30 07:13 apply-raw.lisp -rw-r--r-- 1 kaufmann staff 91128 Oct 30 07:13 apply.lisp -rw-r--r-- 1 kaufmann staff 1079394 Oct 30 07:13 axioms.lisp -rw-r--r-- 1 kaufmann staff 333266 Oct 30 07:13 basis-a.lisp -rw-r--r-- 1 kaufmann staff 30469 Oct 30 07:13 defpkgs.lisp -rw-r--r-- 1 kaufmann staff 439759 Oct 30 07:13 defuns.lisp -rw-r--r-- 1 kaufmann staff 740935 Oct 30 07:13 history-management.lisp -rw-r--r-- 1 kaufmann staff 459477 Oct 30 07:13 interface-raw.lisp -rw-r--r-- 1 kaufmann staff 444069 Oct 30 07:13 simplify.lisp -rw-r--r-- 1 kaufmann staff 589886 Oct 30 07:13 tau.lisp drwxr-xr-x 11 kaufmann staff 352 Oct 30 08:00 logs -rwxrwxr-x 1 kaufmann staff 309 Oct 30 08:02 osaved_acl2 -rw-r--r-- 1 kaufmann staff 1041831 Oct 30 08:02 make-old.log drwxr-xr-x 6 kaufmann staff 192 Oct 31 15:17 bin -rw-r--r-- 1 kaufmann staff 530777 Oct 31 15:17 defthm.lisp -rw-r--r-- 1 kaufmann staff 5145155 Oct 31 15:17 doc.lisp -rw-r--r-- 1 kaufmann staff 1403585 Oct 31 15:17 other-events.lisp -rw-r--r-- 1 kaufmann staff 611982 Oct 31 15:17 translate.lisp -rw-r--r-- 1 kaufmann staff 56 Oct 31 15:17 acl2r.lisp -rw-r--r-- 1 kaufmann staff 350830 Oct 31 15:17 TAGS -rw-r--r-- 1 kaufmann staff 75 Oct 31 15:17 acl2-proclaims.lisp -rw-r--r-- 1 kaufmann staff 12 Oct 31 15:18 acl2-status.txt -rwxrwxr-x 1 kaufmann staff 309 Oct 31 15:18 saved_acl2 -rw-r--r-- 1 kaufmann staff 150712560 Oct 31 15:18 saved_acl2.dx86cl64 drwxrwxr-x 58 kaufmann staff 1856 Oct 31 15:18 saved -rw-r--r-- 1 kaufmann staff 1041884 Oct 31 15:18 make.log drwxr-xr-x 20 kaufmann staff 640 Nov 1 00:49 doc -rw-r--r-- 1 kaufmann staff 1136853 Nov 1 06:41 make-regression-everything-ccl-quicklisp-j-8.log -rw-r--r-- 1 kaufmann staff 38600 Nov 1 08:20 make-regression-everything-ccl-quicklisp-j-8-colors-1.log -rw-r--r-- 1 kaufmann staff 13247 Nov 1 09:32 make-regression-everything-ccl-quicklisp-j-8-colors-2.log -rw-r--r-- 1 kaufmann staff 12778 Nov 1 18:00 make-regression-everything-ccl-quicklisp-j-8-colors-3.log -rw-r--r-- 1 kaufmann staff 38962 Nov 1 19:25 make-regression-everything-ccl-quicklisp-j-8-colors-4.log -rw-r--r-- 1 kaufmann staff 13209 Nov 1 20:27 make-regression-everything-ccl-quicklisp-j-8-colors-5.log drwxr-xr-x 60 kaufmann staff 1920 Nov 1 20:27 books -rw-r--r-- 1 kaufmann staff 7049587 Nov 1 21:07 TAGS-acl2-doc -rw-r--r-- 1 kaufmann staff 16871 Nov 1 21:18 make-regression-everything-ccl-quicklisp-j-8-colors-6.log -rw-r--r-- 1 kaufmann staff 87088 Nov 7 11:11 log.txt.~1~ -rw-r--r-- 1 kaufmann staff 203405 Nov 7 13:42 log.txt ~/acl2/acl2$ make update ACL2_WD is /Users/kaufmann/acl2/acl2 ACL2 is /Users/kaufmann/acl2/acl2/saved_acl2 make: Nothing to be done for `update'. ~/acl2/acl2$ ls -l doc.lisp -rw-r--r-- 1 kaufmann staff 5145155 Oct 31 15:17 doc.lisp ~/acl2/acl2$ acl2 Welcome to Clozure Common Lisp Version 1.12-dev/v1.12-dev.1-3-g1944cfb (DarwinX8664)! ACL2 Version 8.1 built October 31, 2018 15:18:01. Copyright (C) 2018, Regents of the University of Texas ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the LICENSE file distributed with ACL2. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + WARNING: This is NOT an ACL2 release; it is a development snapshot + + (git commit hash: f6e1734a215649017f7a23eb4524f9dc881b720e). + + On rare occasions development snapshots may be incomplete, fragile, + + or unable to pass the usual regression tests. + +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.1. Level 1. Cbd "/Users/kaufmann/acl2/acl2/". System books directory "/Users/kaufmann/acl2/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>:doc rewrite Parent: RULE-CLASSES. Make some :rewrite rules (possibly conditional ones) See [rule-classes] for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description. This doc topic discusses the rule-class :rewrite. If you want a general discussion of how rewriting works in ACL2 and some guidance on how to construct effective rewrite rules, see [introduction-to-rewrite-rules-part-1] and then see [introduction-to-rewrite-rules-part-2]. Examples: (defthm plus-commutes ; Replace (+ a b) by (+ b a) provided (equal (+ x y) (+ y x))) ; certain heuristics approve the ; permutation. (defthm plus-commutes ; equivalent to the above (equal (+ x y) (+ y x)) :rule-classes ((:rewrite :corollary (equal (+ x y) (+ y x)) :loop-stopper ((x y binary-+)) :match-free :all))) (defthm append-nil ; Replace (append a nil) by a, if (implies (true-listp x) ; (true-listp a) rewrites to t. (equal (append x nil) x))) (defthm append-nil ; as above, but with defaults and (implies (true-listp x) ; a backchain limit (equal (append x nil) x)) :rule-classes ((:rewrite :corollary (implies (true-listp x) (equal (append x nil) x)) :backchain-limit-lst (3) ; or equivalently, 3 :match-free :all))) (defthm member-append ; Replace (member e (append b c)) by (implies ; (or (member e b) (member e c) in (and ; contexts in which propositional (true-listp x) ; equivalence is sufficient, provided (true-listp y)) ; b and c are true-lists. (iff (member e (append x y)) (or (member e x) (member e y))))) General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (equiv lhs rhs) ...))) ...) Note: One :rewrite rule class object might create many rewrite rules from the :[corollary] formula. To create the rules, we first translate the formula, expanding all macros (see [trans]) and also removing [guard-holders]. Next, we then flatten the [and] and [implies] structure of the formula; for example, if the hypothesis or conclusion is of the form (and (and term1 term2) term3), then we replace that by the ``flat'' term (and term1 term2 term3). (The latter is actually an abbreviation for the right-associated term (and term1 (and term2 term3)).) During this flattening process, we eliminate [lambda]s as necessary in order to continue flattening; one may think of this step as simply substituting to eliminate [let], [let*], and [mv-let] in order to expose more calls of implies and and. The result is a conjunction of formulas, each of the form (implies (and h1 ... hn) concl) where no hypothesis is a conjunction and concl is neither a conjunction nor an implication. If necessary, the hypothesis of such a conjunct may be vacuous. We then further coerce each concl into the form (equiv lhs rhs), where we continue to eliminate lambdas until we reach this form, and then we eliminate lambdas from the first argument of equiv but not the second argument. Here equiv is a known [equivalence] relation. If we do not reach an equivalence relation, even after eliminating lamdas, then we replace the resulting term, term by (iff term t), except that we replace (not term) by (iff term nil). By these steps we reduce the given :[corollary] to a sequence of conjuncts, each of which is of the form (implies (and h1 ... hn) (equiv lhs rhs)) where equiv is a known [equivalence] relation and lhs has no lambdas. See [equivalence] for a general discussion of the introduction of new [equivalence] relations. At this point, we check whether lhs and rhs are the same term; if so, we cause an error, since this rule will loop. (But this is just a basic check; the rule could loop in other cases, for example if rhs is an instance of lhs; see [loop-stopper].) You can experiment by creating some rewrite rules using [defthm] and then using :[pr] to see how the rule was stored. We create a :rewrite rule for each such conjunct, if possible, and otherwise cause an error. It is possible to create a rewrite rule from such a conjunct provided lhs is not a variable, a quoted constant, a [let]-expression, or a lambda application. Although it is legal to create a rewrite rule from an [if]-expression (if tst tbr fbr), note that the rewriter uses the truth or falsity of the test, tst, when rewriting the true and false branches tbr and fbr, respectively; so rewrite rules are most often unnecessary for if-expressions. A :rewrite rule is used when any instance of the lhs occurs in a context in which the [equivalence] relation is an admissible [congruence] relation. First, we find a substitution that makes lhs equal to the target term. Then we attempt to relieve the instantiated hypotheses of the rule. Hypotheses that are fully instantiated are relieved by recursive rewriting. Hypotheses that contain ``free variables'' (variables not assigned by the unifying substitution) are relieved by attempting to guess a suitable instance so as to make the hypothesis equal to some known assumption in the context of the target. If the hypotheses are relieved, and certain restrictions that prevent some forms of infinite regress are met (see [loop-stopper]), the target is replaced by the instantiated rhs, which is then recursively rewritten. ACL2's rewriting process has some optimizations, including the following. * The notion of ``a substitution that makes lhs equal to the target term'' is a bit more generous than the most straightforward such notion. Suppose for example that lhs is (f (+ 3 x)) and the target term is (f (+ 3 (g y)). (Aside: ACL2 deals in so-called translated terms, so since + is a macro, lhs and term would actually be (f (binary-+ '3 x)) and (f (+ '3 (g y))); we will ignore this distinction, but if you want more information, see [term].) Then of course, that substitution binds x to (g y). But now suppose that instead the target term is (f 10). You may be surprised to learn that the substitution binding x to 7 makes (f (+ 3 x)) equal to (f 10); for example, the rewrite rule (equal (f (+ x 3)) (h x))) would rewrite (f 10) to (h 7). This would also be the case if lhs were instead (f (+ x 3)). This sort of optimization occurs when the new constant has [ACL2-count] no greater than the old constant. There are similar optimizations for *, /, -, strings, symbols, and conses (for details see ACL2 source function one-way-unify1-quotep-subproblems). * When a term t1 is rewritten to a new term t2, the rewriter is then immediately applied to t2. On rare occasions you may find that you do not want this behavior, in which case you may wish to use a trick involving [hide]; see [meta], near the end of that documentation. * When the hypotheses and right-hand side are rewritten, ACL2 does not really first apply the substitution and then rewrite; instead, it as it rewrites those terms it looks up the already rewritten values of the bound variables. Sometimes you may want those bindings rewritten again, e.g., because the variables occur in slots that admit additional equivalence relations. See [double-rewrite]. See [introduction-to-rewrite-rules-part-1] and see [introduction-to-rewrite-rules-part-2] for an extended discussion of how to create effective rewrite rules. Subtopics [Backchain-limit] Limiting the effort expended on relieving hypotheses [Bind-free] To bind free variables of a rewrite, definition, or linear rule [Case-split] Like force but immediately splits the top-level goal on the hypothesis [Double-rewrite] Cause a term to be rewritten twice [Force] Identity function used to force a hypothesis [Free-variables] Free variables in rules [Hide] Hide a term from the rewriter [Loop-stopper] Limit application of permutative rewrite rules [Rewrite-stack-limit] Limiting the stack depth of the ACL2 rewriter [Set-rw-cache-state] Set the default rw-cache-state [Set-rw-cache-state!] Set the default rw-cache-state non-[local]ly [Simple] :[definition] and :[rewrite] rules used in preprocessing [Syntaxp] Attach a heuristic filter on a rule ACL2 !>(include-book "xdoc/top" :dir :system) Summary Form: ( INCLUDE-BOOK "xdoc/top" ...) Rules: NIL Time: 0.11 seconds (prove: 0.00, print: 0.00, other: 0.11) "/Users/kaufmann/acl2/acl2/books/xdoc/top.lisp" ACL2 !>:doc rewrite TTAG NOTE (for included book): Adding ttag :XDOC from book /Users/kaufmann/acl2/acl2/books/xdoc/defxdoc-raw. TTAG NOTE (for included book): Adding ttag :READ-STRING from book /Users/kaufmann/acl2/acl2/books/std/io/read-string. TTAG NOTE (for included book): Adding ttag :UNSOUND-EVAL from book /Users/kaufmann/acl2/acl2/books/xdoc/unsound-eval. TTAG NOTE (for included book): Adding ttag :XDOC from book /Users/kaufmann/acl2/acl2/books/xdoc/defxdoc-raw. TTAG NOTE (for included book): Adding ttag :FAST-CAT from book /Users/kaufmann/acl2/acl2/books/std/strings/fast-cat. Note: not introducing any PREPROC-DATA field bindings for PREPROC-DATA, since none of its fields appear to be used. ACL2::REWRITE -- ACL2 Sources Parents: ACL2::RULE-CLASSES. Make some :rewrite rules (possibly conditional ones) See [rule-classes] for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description. This doc topic discusses the rule-class :rewrite. If you want a general discussion of how rewriting works in ACL2 and some guidance on how to construct effective rewrite rules, see [introduction-to-rewrite-rules-part-1] and then see [introduction-to-rewrite-rules-part-2]. Examples: (defthm plus-commutes ; Replace (+ a b) by (+ b a) provided (equal (+ x y) (+ y x))) ; certain heuristics approve the ; permutation. (defthm plus-commutes ; equivalent to the above (equal (+ x y) (+ y x)) :rule-classes ((:rewrite :corollary (equal (+ x y) (+ y x)) :loop-stopper ((x y binary-+)) :match-free :all))) (defthm append-nil ; Replace (append a nil) by a, if (implies (true-listp x) ; (true-listp a) rewrites to t. (equal (append x nil) x))) (defthm append-nil ; as above, but with defaults and (implies (true-listp x) ; a backchain limit (equal (append x nil) x)) :rule-classes ((:rewrite :corollary (implies (true-listp x) (equal (append x nil) x)) :backchain-limit-lst (3) ; or equivalently, 3 :match-free :all))) (defthm member-append ; Replace (member e (append b c)) by (implies ; (or (member e b) (member e c) in (and ; contexts in which propositional (true-listp x) ; equivalence is sufficient, provided (true-listp y)) ; b and c are true-lists. (iff (member e (append x y)) (or (member e x) (member e y))))) General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (equiv lhs rhs) ...))) ...) Note: One :rewrite rule class object might create many rewrite rules from the :[corollary] formula. To create the rules, we first translate the formula, expanding all macros (see [trans]) and also removing [guard-holders]. Next, we then flatten the [and] and [implies] structure of the formula; for example, if the hypothesis or conclusion is of the form (and (and term1 term2) term3), then we replace that by the ``flat'' term (and term1 term2 term3). (The latter is actually an abbreviation for the right-associated term (and term1 (and term2 term3)).) During this flattening process, we eliminate [lambda]s as necessary in order to continue flattening; one may think of this step as simply substituting to eliminate [let], [let*], and [mv-let] in order to expose more calls of implies and and. The result is a conjunction of formulas, each of the form (implies (and h1 ... hn) concl) where no hypothesis is a conjunction and concl is neither a conjunction nor an implication. If necessary, the hypothesis of such a conjunct may be vacuous. We then further coerce each concl into the form (equiv lhs rhs), where we continue to eliminate lambdas until we reach this form, and then we eliminate lambdas from the first argument of equiv but not the second argument. Here equiv is a known [equivalence] relation. If we do not reach an equivalence relation, even after eliminating lamdas, then we replace the resulting term, term by (iff term t), except that we replace (not term) by (iff term nil). By these steps we reduce the given :[corollary] to a sequence of conjuncts, each of which is of the form (implies (and h1 ... hn) (equiv lhs rhs)) where equiv is a known [equivalence] relation and lhs has no lambdas. See [equivalence] for a general discussion of the introduction of new [equivalence] relations. At this point, we check whether lhs and rhs are the same term; if so, we cause an error, since this rule will loop. (But this is just a basic check; the rule could loop in other cases, for example if rhs is an instance of lhs; see [loop-stopper].) You can experiment by creating some rewrite rules using [defthm] and then using :[pr] to see how the rule was stored. We create a :rewrite rule for each such conjunct, if possible, and otherwise cause an error. It is possible to create a rewrite rule from such a conjunct provided lhs is not a variable, a quoted constant, a [let]-expression, or a lambda application. Although it is legal to create a rewrite rule from an [if]-expression (if tst tbr fbr), note that the rewriter uses the truth or falsity of the test, tst, when rewriting the true and false branches tbr and fbr, respectively; so rewrite rules are most often unnecessary for if-expressions. A :rewrite rule is used when any instance of the lhs occurs in a context in which the [equivalence] relation is an admissible [congruence] relation. First, we find a substitution that makes lhs equal to the target term. Then we attempt to relieve the instantiated hypotheses of the rule. Hypotheses that are fully instantiated are relieved by recursive rewriting. Hypotheses that contain ``free variables'' (variables not assigned by the unifying substitution) are relieved by attempting to guess a suitable instance so as to make the hypothesis equal to some known assumption in the context of the target. If the hypotheses are relieved, and certain restrictions that prevent some forms of infinite regress are met (see [loop-stopper]), the target is replaced by the instantiated rhs, which is then recursively rewritten. ACL2's rewriting process has some optimizations, including the following. * The notion of ``a substitution that makes lhs equal to the target term'' is a bit more generous than the most straightforward such notion. Suppose for example that lhs is (f (+ 3 x)) and the target term is (f (+ 3 (g y)). (Aside: ACL2 deals in so-called translated terms, so since + is a macro, lhs and term would actually be (f (binary-+ '3 x)) and (f (+ '3 (g y))); we will ignore this distinction, but if you want more information, see [term].) Then of course, that substitution binds x to (g y). But now suppose that instead the target term is (f 10). You may be surprised to learn that the substitution binding x to 7 makes (f (+ 3 x)) equal to (f 10); for example, the rewrite rule (equal (f (+ x 3)) (h x))) would rewrite (f 10) to (h 7). This would also be the case if lhs were instead (f (+ x 3)). This sort of optimization occurs when the new constant has [ACL2-count] no greater than the old constant. There are similar optimizations for *, /, -, strings, symbols, and conses (for details see ACL2 source function one-way-unify1-quotep-subproblems). * When a term t1 is rewritten to a new term t2, the rewriter is then immediately applied to t2. On rare occasions you may find that you do not want this behavior, in which case you may wish to use a trick involving [hide]; see [meta], near the end of that documentation. * When the hypotheses and right-hand side are rewritten, ACL2 does not really first apply the substitution and then rewrite; instead, it as it rewrites those terms it looks up the already rewritten values of the bound variables. Sometimes you may want those bindings rewritten again, e.g., because the variables occur in slots that admit additional equivalence relations. See [double-rewrite]. See [introduction-to-rewrite-rules-part-1] and see [introduction-to-rewrite-rules-part-2] for an extended discussion of how to create effective rewrite rules. Subtopics [Backchain-limit] Limiting the effort expended on relieving hypotheses [Bind-free] To bind free variables of a rewrite, definition, or linear rule [Case-split] Like force but immediately splits the top-level goal on the hypothesis [Double-rewrite] Cause a term to be rewritten twice [Force] Identity function used to force a hypothesis [Free-variables] Free variables in rules [Hide] Hide a term from the rewriter [Loop-stopper] Limit application of permutative rewrite rules [Rewrite-stack-limit] Limiting the stack depth of the ACL2 rewriter [Set-rw-cache-state] Set the default rw-cache-state [Set-rw-cache-state!] Set the default rw-cache-state non-[local]ly [Simple] :[definition] and :[rewrite] rules used in preprocessing [Syntaxp] Attach a heuristic filter on a rule ACL2 !>Bye. ~/acl2/acl2$ alias make-doc alias make-doc='mv make-doc.log make-doc-old.log ; (time nice make DOC large check-acl2-exports LISP=ccl ACL2=`pwd`/saved_acl2) >& make-doc.log&' ~/acl2/acl2$ acl2 Welcome to Clozure Common Lisp Version 1.12-dev/v1.12-dev.1-3-g1944cfb (DarwinX8664)! ACL2 Version 8.1 built October 31, 2018 15:18:01. Copyright (C) 2018, Regents of the University of Texas ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the LICENSE file distributed with ACL2. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + WARNING: This is NOT an ACL2 release; it is a development snapshot + + (git commit hash: f6e1734a215649017f7a23eb4524f9dc881b720e). + + On rare occasions development snapshots may be incomplete, fragile, + + or unable to pass the usual regression tests. + +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.1. Level 1. Cbd "/Users/kaufmann/acl2/acl2/". System books directory "/Users/kaufmann/acl2/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defpkg "FOO" '(a)) Summary Form: ( DEFPKG "FOO" ...) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) "FOO" ACL2 !>(thm (equal (symbol-package-name (intern$ "A" "FOO")) "ACL2")) Q.E.D. Summary Form: ( THM ...) Rules: ((:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTERN-IN-PACKAGE-OF-SYMBOL) (:EXECUTABLE-COUNTERPART PKG-WITNESS) (:EXECUTABLE-COUNTERPART SYMBOL-PACKAGE-NAME)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 7 Proof succeeded. ACL2 !>Bye. ~/acl2/acl2$ acl2 Welcome to Clozure Common Lisp Version 1.12-dev/v1.12-dev.1-3-g1944cfb (DarwinX8664)! ACL2 Version 8.1 built October 31, 2018 15:18:01. Copyright (C) 2018, Regents of the University of Texas ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the LICENSE file distributed with ACL2. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + WARNING: This is NOT an ACL2 release; it is a development snapshot + + (git commit hash: f6e1734a215649017f7a23eb4524f9dc881b720e). + + On rare occasions development snapshots may be incomplete, fragile, + + or unable to pass the usual regression tests. + +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.1. Level 1. Cbd "/Users/kaufmann/acl2/acl2/". System books directory "/Users/kaufmann/acl2/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defpkg "FOO" '()) Summary Form: ( DEFPKG "FOO" ...) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) "FOO" ACL2 !>(thm (not (equal (symbol-package-name (intern$ "A" "FOO")) "ACL2"))) Q.E.D. Summary Form: ( THM ...) Rules: ((:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTERN-IN-PACKAGE-OF-SYMBOL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART PKG-WITNESS) (:EXECUTABLE-COUNTERPART SYMBOL-PACKAGE-NAME)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 8 Proof succeeded. ACL2 !>Bye. ~/acl2/acl2$ acl2 Welcome to Clozure Common Lisp Version 1.12-dev/v1.12-dev.1-3-g1944cfb (DarwinX8664)! ACL2 Version 8.1 built October 31, 2018 15:18:01. Copyright (C) 2018, Regents of the University of Texas ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the LICENSE file distributed with ACL2. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + WARNING: This is NOT an ACL2 release; it is a development snapshot + + (git commit hash: f6e1734a215649017f7a23eb4524f9dc881b720e). + + On rare occasions development snapshots may be incomplete, fragile, + + or unable to pass the usual regression tests. + +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.1. Level 1. Cbd "/Users/kaufmann/acl2/acl2/". System books directory "/Users/kaufmann/acl2/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(set-debugger-enable t) ACL2 !>(car 3) ACL2 Error in TOP-LEVEL: The guard for the function call (CAR X), which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CAR 3). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !> C-c C-c> Break: interrupt signal > While executing: CCL::FD-READ, in process listener(1). > Type :GO to continue, :POP to abort, :R for a list of available restarts. > If continued: Return from BREAK. > Type :? for other options. 1 > *features* (:RDTSC :CLTL2 :STATIC-HONS :ACL2-MV-AS-VALUES :HONS :PRIMARY-CLASSES :COMMON-LISP :OPENMCL :CCL :CCL-1.2 :CCL-1.3 :CCL-1.4 :CCL-1.5 :CCL-1.6 :CCL-1.7 :CCL-1.8 :CCL-1.9 :CCL-1.10 :CCL-1.11 :CCL-1.12 :CLOZURE :CLOZURE-COMMON-LISP :ANSI-CL :UNIX :OPENMCL-UNICODE-STRINGS :IPV6 :OPENMCL-NATIVE-THREADS :OPENMCL-PARTIAL-MOP :MCL-COMMON-MOP-SUBSET :OPENMCL-MOP-2 :OPENMCL-PRIVATE-HASH-TABLES :STATIC-CONSES-SHOULD-WORK-WITH-EGC-IN-CCL :X86-64 :X86_64 :X86-TARGET :X86-HOST :X8664-TARGET :X8664-HOST :DARWIN-HOST :DARWIN-TARGET :DARWINX86-TARGET :DARWINX8664-TARGET :DARWINX8664-HOST :64-BIT-TARGET :64-BIT-HOST :DARWIN :LITTLE-ENDIAN-TARGET :LITTLE-ENDIAN-HOST) 1 > :q ACL2 !>:q Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ? (LP!) ACL2 Version 8.1. Level 1. Cbd "/Users/kaufmann/acl2/acl2/". System books directory "/Users/kaufmann/acl2/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> C-c C-c > Break: interrupt signal > While executing: CCL::FD-READ, in process listener(1). > Type :GO to continue, :POP to abort, :R for a list of available restarts. > If continued: Return from BREAK. > Type :? for other options. 1 > *re > Error: Unbound variable: *RE > While executing: CCL::TOPLEVEL-EVAL, in process listener(1). > Type :GO to continue, :POP to abort, :R for a list of available restarts. > If continued: Retry getting the value of *RE. > Type :? for other options. 2 > *features* (:ACL2-LOOP-ONLY :RDTSC :CLTL2 :STATIC-HONS :ACL2-MV-AS-VALUES :HONS :PRIMARY-CLASSES :COMMON-LISP :OPENMCL :CCL :CCL-1.2 :CCL-1.3 :CCL-1.4 :CCL-1.5 :CCL-1.6 :CCL-1.7 :CCL-1.8 :CCL-1.9 :CCL-1.10 :CCL-1.11 :CCL-1.12 :CLOZURE :CLOZURE-COMMON-LISP :ANSI-CL :UNIX :OPENMCL-UNICODE-STRINGS :IPV6 :OPENMCL-NATIVE-THREADS :OPENMCL-PARTIAL-MOP :MCL-COMMON-MOP-SUBSET :OPENMCL-MOP-2 :OPENMCL-PRIVATE-HASH-TABLES :STATIC-CONSES-SHOULD-WORK-WITH-EGC-IN-CCL :X86-64 :X86_64 :X86-TARGET :X86-HOST :X8664-TARGET :X8664-HOST :DARWIN-HOST :DARWIN-TARGET :DARWINX86-TARGET :DARWINX8664-TARGET :DARWINX8664-HOST :64-BIT-TARGET :64-BIT-HOST :DARWIN :LITTLE-ENDIAN-TARGET :LITTLE-ENDIAN-HOST) 2 > ACACL2 !> ~/acl2/acl2$