[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: address@hidden: Re: [Gcl-devel] Re: Profiling [ was Re: lisp reader
From: |
Matt Kaufmann |
Subject: |
Re: address@hidden: Re: [Gcl-devel] Re: Profiling [ was Re: lisp reader enhancement ]] |
Date: |
Tue, 12 Aug 2003 11:44:00 -0500 |
Hi, Camm --
OK, I've re-run the test. The shell command was as follows. Here and below,
"..." indicates an omitted full pathname.
(time .../gcl-saved_acl2) < test.lsp >& test.log&
Below is the top-level test file test.lsp, followed by relevant parts of the
(very large) test.log. It doesn't look to me like the gprof info will be very
helpful, unfortunately. By the way, heap_end changed slightly after I rebuilt
ACL2 on the GCL that incorporates the latest patch you sent, but that shouldn't
matter, since (/ (- 154484736 #x8049cb0) 1000000.0) is now 19.964752, which
means that the second argument I gave to si::prof, namely 20, is still
appropriate.
++++++++++++++++++++++++++++++ test.lsp ++++++++++++++++++++++++++++++
(value :q) ; exit ACL2 loop
(room t)
; Allocate extra room.
(sloop::sloop for (type . n) in
'((hole . 500) ; unchanged
(relocatable . 750) ; was 500
(cons . 60000) ; was 2917
(fixnum . 250) ; was 100
(bignum . 400) ; unchanged
(symbol . 900) ; was 400
(array . 40) ; was unassigned
(string . 2000); was 200
(sfun . 60) ; was 40
)
when n
do
(cond
((eq type 'HOLE)
(si::set-hole-size n))
((eq type 'RELOCATABLE)
(si::allocate-relocatable-pages n))
(t (si::allocate type n t))))
(room t)
(si::gbc-time 0)
(format t "*** Internal time: ~s~%" (get-internal-run-time))
(format t "*** Internal-time-units-per-second: ~s~%"
internal-time-units-per-second)
#|
I did the following, which seemed to give me _init and heap_end:
[ 295 ] --> gdb .../gcl-saved_acl2
GNU gdb 5.3
Copyright 2002 Free Software Foundation, Inc.
GDB is free software, covered by the GNU General Public License, and you are
welcome to change it and/or distribute copies of it under certain conditions.
Type "show copying" to see the conditions.
There is absolutely no warranty for GDB. Type "show warranty" for details.
This GDB was configured as "i686-pc-linux-gnu"...
(gdb) p _init
$1 = {<text variable, no debug info>} 0x8049cb0 <_init>
(gdb) p heap_end
$2 = 155021312
(gdb)
|#
(si::set-up-profile 1000000 8000) ; ACL2 has about 4100 defuns and about 600
macros
; >(/ (- 155021312 #x8049cb0) 1000000.0)
; ;heap_end ;_init
; 20.501328000000001
(si::prof #x8049cb0 20)
(lp) ; enter ACL2 read-eval-print loop
(ld "pkgs.lisp") ; some constant and package definitions
;; New!
(assign inhibit-output-lst
(list (quote prove) (quote proof-tree) (quote warning)
(quote observation) (quote event) (quote summary)))
(certify-book "model-eq" ?) ; the main test
(value :q) ; exit ACL2 loop
(format t "*** Internal time: ~s~%" (get-internal-run-time))
(si::gbc-time)
(room t)
(si::prof 0 0)
(si::display-profile #x8049cb0 20)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
++++++++++++++++++++++++++++++ test.log (portions)
++++++++++++++++++++++++++++++
GCL (GNU Common Lisp) (2.5.3) Tue Aug 12 09:40:19 CDT 2003
Licensed under GNU Library General Public License
Dedicated to the memory of W. Schelter
Use (help) to get some basic information on how to use GCL.
ACL2 Version 2.8 built August 12, 2003 09:46:12.
Copyright (C) 2003 University of Texas at Austin
ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you
are welcome to redistribute it under certain conditions. For details,
see the GNU General Public License.
Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES* T).
See the documentation topic note-2-8 for recent changes.
NOTE!! Proof trees are disabled in ACL2. To enable them in emacs,
look under the ACL2 source directory in interface/emacs/README.doc;
and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2
command loop. Look in the ACL2 documentation under PROOF-TREE.
ACL2 Version 2.8. Level 1. Cbd ".../gcl-test/".
Type :help for help.
ACL2 !>
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>2917/2917 82.4%CONS RATIO LONG-FLOAT COMPLEX STRUCTURE
100/100 18.3% FIXNUM SHORT-FLOAT CHARACTER RANDOM-STATE READTABLE NIL
400/400 35.2% SYMBOL STREAM
1/2 37.2% PACKAGE
5/38 14.0% ARRAY HASH-TABLE VECTOR BIT-VECTOR PATHNAME CCLOSURE
FAT-STRING
200/200 46.4% STRING
400/400 1.8% CFUN BIGNUM
40/40 56.7% SFUN GFUN CFDATA SPICE NIL
1/100 contiguous (1 blocks)
1000 hole
500 0.1% relocatable
4063 pages for cells
5564 total pages
119225 pages available
6283 pages in heap but not gc'd + pages needed for gc marking
131072 maximum pages
ACL2>[SGC off][GC for 750 RELOCATABLE-BLOCKS pages..(T=13).GC finished]
[SGC on][SGC off][GC for 750 RELOCATABLE-BLOCKS pages..(T=53).GC finished]
[SGC on][SGC off][GC for 750 RELOCATABLE-BLOCKS pages..(T=54).GC finished]
[SGC on]
NIL
ACL2>60000/60000 95.0%CONS RATIO LONG-FLOAT COMPLEX STRUCTURE
250/250 7.3% FIXNUM SHORT-FLOAT CHARACTER RANDOM-STATE READTABLE NIL
900/900 15.6% SYMBOL STREAM
1/2 37.2% PACKAGE
40/40 1.5% ARRAY HASH-TABLE VECTOR BIT-VECTOR PATHNAME CCLOSURE
FAT-STRING
2000/2000 4.6% STRING
400/400 1.8% CFUN BIGNUM
60/60 37.8% SFUN GFUN CFDATA SPICE NIL
1/100 3 contiguous (1 blocks)
480 hole
750 0.0% 3 relocatable
63651 pages for cells
64882 total pages
59137 pages available
7053 pages in heap but not gc'd + pages needed for gc marking
131072 maximum pages
ACL2>
0
ACL2>*** Internal time: 642
NIL
ACL2>*** Internal-time-units-per-second: 100
NIL
ACL2>
Loading .../gcl-2.5.3/lsp/profile.lsp
Finished loading .../gcl-2.5.3/lsp/profile.lsp
"making new array" [SGC for 0 CONTIGUOUS-BLOCKS pages..(7139
writable)..(T=12).GC finished]
[SGC for 0 CONTIGUOUS-BLOCKS pages..(9200 writable)..(T=11).GC finished]
[SGC for 0 CONTIGUOUS-BLOCKS pages..(9200 writable)..(T=11).GC finished]
Loaded c and other function addresses
Using profile-array length 1000000
Use (si::prof 0 90) to start and (prof 0 0) to stop:
This starts monitoring at address 0
thru byte (256/90)*(length *profile-array*)
(si::display-prof) displays the results
NIL
ACL2>
134519984
ACL2>
ACL2 Version 2.8. Level 1. Cbd ".../gcl-test/".
Type :help for help.
<<< lots of output omitted >>>
ACL2 !>
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>*** Internal time: 526271
NIL
ACL2>
39895
ACL2>78000/78000 99.5%202CONS RATIO LONG-FLOAT COMPLEX STRUCTURE
250/250 68.8% 69 FIXNUM SHORT-FLOAT CHARACTER RANDOM-STATE READTABLE NIL
900/900 89.3% SYMBOL STREAM
1/2 64.1% PACKAGE
40/40 2.2% 55 ARRAY HASH-TABLE VECTOR BIT-VECTOR PATHNAME CCLOSURE
FAT-STRING
2000/2000 22.0% STRING
400/400 5.5% 10 CFUN BIGNUM
60/60 69.6% SFUN GFUN CFDATA SPICE NIL
6713/7553 1309contiguous (17 blocks)
490 hole
750 17.4%1309relocatable
81651 pages for cells
89604 total pages
34425 pages available
7043 pages in heap but not gc'd + pages needed for gc marking
131072 maximum pages
ACL2>
0
ACL2>
0.00% ( 1): _IO_getc
0.01% ( 3): NewInit
0.10% ( 28): IapplyVector
0.56% ( 160): Iinvoke_c_function_from_value_stack
0.03% ( 9): make_ratio
0.01% ( 3): make_fixnum1
0.00% ( 1): fixint
0.06% ( 16): fixnnint
1.40% ( 404): number_compare
0.00% ( 1): Lmonotonically_nondecreasing
0.01% ( 4): Lfloor
0.01% ( 4): Lceiling
0.00% ( 1): Lmod
0.00% ( 1): Lminusp
0.01% ( 3): number_zerop
0.01% ( 3): number_plusp
0.02% ( 7): number_minusp
0.00% ( 1): number_evenp
0.00% ( 1): number_expt
0.02% ( 5): Lexpt
1.82% ( 525): find_package
0.36% ( 103): pack_hash
1.58% ( 455): intern
0.03% ( 9): find_symbol
0.05% ( 14): Lrename_package
0.13% ( 36): Lintern
0.01% ( 2): current_package
0.09% ( 26): Lfind_package
0.08% ( 23): Lpackage_name
1.69% ( 487): eql
1.56% ( 450): equal
0.00% ( 1): equalp
0.00% ( 1): fLlistp
0.01% ( 2): fLintegerp
0.02% ( 5): fLrationalp
0.01% ( 3): fLcomplexp
0.01% ( 2): Lcomplexp
0.01% ( 2): Lsimple_string_p
0.00% ( 1): Latom
0.00% ( 1): edit_double
0.03% ( 10): write_object
0.01% ( 3): setupPRINTdefault
0.03% ( 8): princ
0.00% ( 1): Lforce_output
0.01% ( 2): Lterpri
0.01% ( 2): writec_PRINTstream
0.01% ( 2): Fprogn
0.01% ( 2): rl_getc_em
0.01% ( 3): rl_putc_em
0.00% ( 1): read_object_non_recursive
0.55% ( 159): read_object
0.06% ( 17): NIL
0.00% ( 1): NIL
0.02% ( 5): Lsymbol_function
0.01% ( 2): symbol_function
0.35% ( 100): Lfboundp
0.00% ( 1): Lsymbol_value
0.01% ( 2): Lmacro_function
0.00% ( 1): Lspecial_form_p
0.78% ( 225): elt
1.59% ( 457): elt_set
0.28% ( 81): Llength
0.06% ( 17): reverse
0.03% ( 9): nreverse
0.10% ( 30): init_sequence_function
0.31% ( 89): length
0.03% ( 9): Lcopy_seq
0.34% ( 99): coerce_to_string
0.04% ( 12): Lstring_eq
0.11% ( 32): Lstring_equal
0.01% ( 3): make_simple_string
0.00% ( 1): copy_simple_string
2.19% ( 631): string_equal
0.12% ( 34): string_eq
0.02% ( 5): get_string_start_end
0.01% ( 2): Lstring_l
0.01% ( 2): remf
1.14% ( 327): symbol_name
0.01% ( 3): Lgensym
0.00% ( 1): init_symbol_function
0.02% ( 6): make_si_constant
0.03% ( 8): symbol_value
0.01% ( 3): getf
1.27% ( 366): get
0.00% ( 1): putf
0.01% ( 2): putprop
0.07% ( 21): sputprop
0.01% ( 2): remprop
0.04% ( 11): Lsymbol_package
0.01% ( 2): siLrem_f
0.02% ( 6): check_type_integer
0.07% ( 20): check_type_non_negative_integer
0.13% ( 38): check_type_number
0.03% ( 10): check_type_character
0.02% ( 7): check_type_symbol
0.02% ( 5): check_type_package
0.17% ( 49): check_type_string
0.00% ( 1): check_type_stream
0.01% ( 2): Lget_internal_run_time
0.03% ( 9): __gmpz_set_si
0.09% ( 27): alloc_page
1.04% ( 299): alloc_object
0.75% ( 216): make_cons
0.26% ( 75): fSallocated
0.11% ( 33): alloc_contblock
0.20% ( 57): alloc_relblock
0.03% ( 10): insert_contblock
0.02% ( 6): fSaset
0.22% ( 62): fSmake_vector1
0.41% ( 119): fSmake_vector
0.41% ( 118): gset
0.41% ( 118): array_allocself
0.03% ( 10): siLmake_vector
0.01% ( 2): Lsvref
0.01% ( 3): clear_compiler_properties
0.01% ( 2): fLset
0.01% ( 2): fLmakunbound
0.00% ( 1): fSclear_compiler_properties
0.01% ( 3): setq
0.00% ( 1): Lset
0.01% ( 2): bds_unwind
0.02% ( 5): make_integer
0.02% ( 5): maybe_replace_big
0.05% ( 13): integer_quotient_remainder_1
0.00% ( 1): add_int_big
0.00% ( 1): mul_int_big
0.00% ( 1): init_big
0.00% ( 1): set_big_sign
0.01% ( 2): zero_big
0.00% ( 1): obj_to_mpz1
0.01% ( 3): otoi
0.09% ( 27): lambda_bind
0.01% ( 4): bind_var
0.01% ( 3): find_special
0.03% ( 8): parse_key
0.22% ( 62): parse_key_new_new
0.01% ( 2): set_key_struct
0.01% ( 3): make_cclosure_new
0.07% ( 19): Lcode_char
0.00% ( 1): Lmake_char
0.04% ( 12): Lchar_code
0.02% ( 5): do_init
0.34% ( 97): SYSTEM:IHS-TOP
0.35% ( 101): funcall
0.03% ( 10): funcall_no_event
0.00% ( 1): lispcall
0.21% ( 60): eval
0.01% ( 2): fLfuncall
0.00% ( 1): ifuncall2
0.00% ( 1): ifuncall3
0.00% ( 1): Ieval
0.01% ( 2): fLeval
0.01% ( 4): super_funcall
0.24% ( 69): super_funcall_no_event
0.02% ( 7): Leval
0.01% ( 3): SYSTEM:CLOSE-FASD
0.01% ( 2): readc_stream
0.02% ( 5): unreadc_stream
0.03% ( 10): writec_stream
0.00% ( 1): flush_stream
0.01% ( 2): make_string_input_stream
0.00% ( 1): load
0.02% ( 7): coerce_stream
0.01% ( 2): fLformat
0.00% ( 1): unwind
0.10% ( 28): fSuse_fast_links
0.29% ( 83): c_apply_n
0.00% ( 1): call_proc_new
0.29% ( 83): call_or_link
0.02% ( 5): clear_stack
3.11% ( 896): SYSTEM:MV-REF
0.12% ( 34): GBC
13.12% ( 3775): SYSTEM:ROOM-REPORT
1.06% ( 305): sgc_start
0.73% ( 211): sgc_quit
0.01% ( 4): memory_protect
0.18% ( 51): sgc_count_type
0.00% ( 1): make_writable
2.09% ( 602): init_GBC
0.09% ( 27): SYSTEM:RESET-GBC-COUNT
0.03% ( 10): SYSTEM:GBC-TIME
0.00% ( 1): SYSTEM:SGC-ON
0.00% ( 1): init_iteration
0.01% ( 4): let_var_list
0.01% ( 2): init_let
0.01% ( 4): assoc_eq
0.09% ( 26): init_lex
1.17% ( 338): list
0.08% ( 24): listA
0.05% ( 15): append
0.00% ( 1): Lcadddr
0.01% ( 2): nth
0.00% ( 1): Llast
0.06% ( 17): Lrevappend
0.03% ( 8): Lbutlast
0.04% ( 12): SYSTEM:MEMBER1
0.30% ( 87): car
0.27% ( 77): cdr
0.04% ( 11): kar
0.00% ( 1): cdar
0.00% ( 1): cddr
0.00% ( 1): cadar
0.00% ( 1): cdddr
0.00% ( 1): nthcdr
0.03% ( 9): sublis1
0.09% ( 25): list_vector_new
0.00% ( 1): Llist
0.01% ( 4): LlistA
0.01% ( 3): Lmember_if
0.00% ( 1): SYSTEM:DEFINE-MACRO
0.04% ( 11): macro_expand
0.01% ( 2): Lmacroexpand
0.08% ( 22): fixnum_add
0.01% ( 3): fixnum_sub
0.29% ( 84): number_plus
0.03% ( 9): one_plus
0.02% ( 6): number_minus
0.06% ( 16): one_minus
0.02% ( 5): number_negate
0.02% ( 5): number_times
0.02% ( 7): number_divide
0.01% ( 4): get_gcd
0.03% ( 8): integer_divide1
0.17% ( 48): Lplus
0.00% ( 1): Ldivide
0.00% ( 1): init_num_arith
0.03% ( 9): build_symbol_table
0.81% ( 234): SYSTEM::BEST-ARRAY-ELEMENT-TYPE
0.01% ( 2): COMPILER::COMPILER-DEF-HOOK
0.01% ( 3): SYSTEM::GET-&ENVIRONMENT
0.00% ( 1): SYSTEM:DEFMACRO*
0.00% ( 1): SYSTEM::DM-VL
0.00% ( 1): SYSTEM::DM-V
0.01% ( 4): SYSTEM::DM-NTH-CDR
0.01% ( 3): SYSTEM::FIND-DOC
0.01% ( 2): init_iolib
0.00% ( 1): SYSTEM::KEY-LIST
0.02% ( 6): SUBSETP
0.00% ( 1): ABS
0.01% ( 2): #:G1384
0.13% ( 38): TYPEP
0.79% ( 228): SYSTEM::NORMALIZE-TYPE
2.19% ( 630): SYSTEM::KNOWN-TYPE-P
2.17% ( 624): SUBTYPEP
0.01% ( 3): COERCE
0.05% ( 13): SYSTEM:WARN-VERSION
0.15% ( 44): #:G1380
0.02% ( 5): #:G1381
0.09% ( 26): SYSTEM::CLASS-OF
0.18% ( 52): SYSTEM::CLASSP
0.00% ( 1): SYSTEM::THE-END
0.02% ( 5): init_seqlib
0.21% ( 60): MAKE-SEQUENCE
1.86% ( 536): CONCATENATE
0.00% ( 1): MAP
0.01% ( 3): COMPILER::COMPILER-CLEAR-COMPILER-PROPERTIES
0.01% ( 2): __gmpz_add
0.02% ( 5): __gmpz_add_ui
0.03% ( 9): __gmpz_fits_sint_p
0.01% ( 3): __gmpz_get_si
0.00% ( 1): __gmpz_init
0.00% ( 1): __gmpz_mul
0.01% ( 2): __gmpz_mul_si
0.01% ( 2): __gmpz_set_ui
0.04% ( 11): __gmpz_sub_ui
0.02% ( 5): __gmpz_tdiv_qr
0.00% ( 1): __gmpn_sub_n
0.01% ( 4): __gmpn_mul_1
0.02% ( 7): __gmpn_tdiv_qr
0.01% ( 4): __gmpn_divrem_1c
0.01% ( 2): __gmpn_divrem_1
0.01% ( 3): bfd_getb32
0.00% ( 1): bfd_get_section_contents
0.01% ( 4): bfd_elf32_slurp_symbol_table
0.00% ( 1): bfd_elf_generic_reloc
0.00% ( 1): _bfd_elf_canonicalize_reloc
0.00% ( 1): bfd_get_arch
0.00% ( 1): bfd_lookup_arch
0.00% ( 1): bfd_printable_arch_mach
0.01% ( 2): bfd_arch_mach_octets_per_byte
0.01% ( 3): bfd_check_overflow
0.03% ( 10): bfd_perform_relocation
0.00% ( 1): COLLECT-TYPES
0.00% ( 1): PROCLAIM-FORM
0.49% ( 142): SYMBOL-PACKAGE-NAME
0.01% ( 3): REV1@
0.07% ( 20): GLOBAL-SYMBOL
0.20% ( 58): *1*-SYMBOL
0.06% ( 16): DEFUN-*1*
0.01% ( 4): EVAL-GROUND-SUBEXPRESSIONS
0.00% ( 1): LINEARIZE1
0.01% ( 2): ADD-TYPE-SET-POLYS
0.00% ( 1): LINEARIZE
0.00% ( 1): LINEARIZE-LST
0.01% ( 4): PUSH-WORMHOLE-UNDO-FORMI
0.00% ( 1): ACL2-COUNT
0.01% ( 4): COND-CLAUSESP
0.02% ( 5): PSEUDO-TERMP
0.00% ( 1): SYMBOL-<
0.14% ( 39): ACL2-UNWIND
1.80% ( 517): SGETPROP1
1.70% ( 490): FGETPROP
0.00% ( 1): HAS-PROPSP
0.66% ( 191): AREF1
0.76% ( 219): COMPRESS1
0.01% ( 2): AREF2
0.00% ( 1): WRITABLE-FILE-LISTP1
0.02% ( 7): GLOBAL-TABLE-CARS1
0.05% ( 15): BOUNDP-GLOBAL1
0.00% ( 1): MAKUNBOUND-GLOBAL
0.00% ( 1): GET-GLOBAL
0.01% ( 2): F-GET-GLOBAL
0.01% ( 2): PUT-GLOBAL
0.00% ( 1): STATE-GLOBAL-LET*-GET-GLOBALS
0.01% ( 2): OPEN-INPUT-CHANNEL-P1
0.06% ( 16): PRINC$
0.02% ( 7): MAY-NEED-SLASHES
0.14% ( 40): ASET-32-BIT-INTEGER-STACK
0.00% ( 1): IDATE
0.01% ( 3): READ-RUN-TIME
0.02% ( 7): MAIN-TIMER
0.00% ( 1): SET-TIMER
0.02% ( 6): PRIN1$
0.04% ( 11): SET-W
0.16% ( 47): BAD-LISP-OBJECTP
0.00% ( 1): WORMHOLE1
0.00% ( 1): ALPHORDER
0.00% ( 1): ACL2-NUMBERP
0.01% ( 2): FIND-PACKAGE-FAST
0.01% ( 4): IMPLIES
0.14% ( 39): TRUE-LISTP
0.00% ( 1): OR-MACRO
0.01% ( 2): LEN
0.02% ( 5): ALISTP
0.09% ( 25): MEMBER-EQUAL
0.02% ( 7): SYMBOL-LISTP
0.08% ( 24): MEMBER-EQ
0.11% ( 33): SUBSETP-EQ
0.00% ( 1): SYMBOL-ALISTP
0.93% ( 269): ASSOC-EQ
0.39% ( 113): ASSOC-EQUAL
0.05% ( 13): ASSOC-EQ-EQUAL-ALISTP
0.05% ( 14): ASSOC-EQ-EQUAL
0.00% ( 1): NO-DUPLICATESP-EQUAL
0.01% ( 4): STRIP-CARS1
0.01% ( 3): STRIP-CARS
0.00% ( 1): ZP
0.33% ( 96): PROG2$
0.00% ( 1): NO-DUPLICATESP
0.01% ( 3): MEMBER-SYMBOL-NAME
0.00% ( 1): INTERN-IN-PACKAGE-OF-SYMBOL
0.00% ( 1): BINARY-APPEND
0.01% ( 3): STRING-APPEND
0.02% ( 5): STRING-APPEND-LST
0.02% ( 5): PAIRLIS$
0.00% ( 1): REMOVE-DUPLICATES-EQL
0.01% ( 3): SET-DIFFERENCE-EQ
0.01% ( 2): STRIP-CDRS1
0.00% ( 1): PSEUDO-TERM-LISTP
0.01% ( 4): ADD-TO-SET-EQ
0.00% ( 1): ADD-TO-SET-EQL
0.05% ( 14): QUOTEP
0.00% ( 1): KWOTE
0.01% ( 3): FN-SYMB
0.11% ( 33): ALL-VARS1
0.03% ( 8): ALL-VARS1-LST
0.01% ( 2): ALL-VARS
0.01% ( 3): INTERSECTP-EQ
0.01% ( 2): MAKE-FMT-BINDINGS
0.01% ( 3): PUTPROP
0.08% ( 24): GETPROP-DEFAULT
0.92% ( 266): SGETPROP
0.01% ( 2): GETPROPS1
0.01% ( 3): GLOBAL-VAL
0.02% ( 5): ASSOC-KEYWORD
0.01% ( 2): HEADER
0.00% ( 1): MV-NTH
0.01% ( 2): COERCE-STATE-TO-OBJECT
0.01% ( 4): BOUNDP-GLOBAL
0.00% ( 1): EXPLODE-NONNEGATIVE-INTEGER
0.00% ( 1): OPEN-INPUT-CHANNEL-P
0.02% ( 5): ASET-T-STACK
0.01% ( 4): 32-BIT-INTEGER-STACK-LENGTH1
0.02% ( 7): 32-BIT-INTEGER-STACK-LENGTH
0.05% ( 15): AREF-32-BIT-INTEGER-STACK
0.02% ( 7): USER-STOBJ-ALIST
0.00% ( 1): READ-IDATE
0.01% ( 4): PUT-ASSOC-EQ
0.01% ( 3): GET-TIMER
0.01% ( 4): PUSH-TIMER
0.02% ( 5): POP-TIMER
0.00% ( 1): INCREMENT-TIMER
0.03% ( 8): W
0.00% ( 1): KNOWN-PACKAGE-ALIST
0.01% ( 4): UNION-EQ
0.01% ( 4): LD-SKIP-PROOFSP
0.02% ( 6): CHK-BAD-LISP-OBJECT
0.02% ( 6): TABLE-ALIST
0.00% ( 1): GOOD-DEFUN-MODE-P
0.01% ( 2): DEFAULT-DEFUN-MODE-FROM-STATE
0.00% ( 1): LET*-ABSTRACTIONP
0.01% ( 2): DEFAULT-BACKCHAIN-LIMIT
0.01% ( 2): DEFAULT-HINTS
0.00% ( 1): MATCH-FREE-OVERRIDE
0.00% ( 1): PAIRLIS2
0.00% ( 1): ADD-TO-SET-EQUAL
0.00% ( 1): INTERSECTION-EQ
0.04% ( 11): EVENS
0.01% ( 2): LEXORDER
0.02% ( 7): E/D-FN
0.01% ( 3): CONVERT-TYPE-SET-TO-TERM-LST
0.00% ( 1): SUBLIS-EXPR
0.01% ( 2): TYPE-SET-<-ALIST
0.00% ( 1): MOVE-UNMARKED-SUBBTREES
0.00% ( 1): ACCUMULATE-TTREE-INTO-STATE
0.02% ( 7): FN-COUNT-EVG-REC
0.00% ( 1): ADD-LINEAR-VARIABLE
0.01% ( 2): ALL-QUOTEPS
1.43% ( 412): TAG-TREE-OCCUR
0.09% ( 27): ADD-TO-TAG-TREE
0.04% ( 12): PUSH-LEMMA
0.01% ( 4): PUSH-LEMMAS
0.01% ( 3): ADD-TO-SET-EQ-IN-ALIST
0.01% ( 4): TAGGED-OBJECTS
0.01% ( 3): TAGGED-OBJECT
0.00% ( 1): MARRY-PARENTS
0.00% ( 1): FORCE-ASSUMPTION
0.00% ( 1): FILTER-POLYS
0.01% ( 3): NEW-VARS-IN-POT-LST
0.12% ( 34): LEGAL-VARIABLE-OR-CONSTANT-NAMEP
0.02% ( 6): FLSZ-ATOM
0.01% ( 4): PPR1
0.00% ( 1): FLPR11
0.02% ( 7): PPR2-FLAT
0.00% ( 1): PPR
0.00% ( 1): FIND-ALTERNATIVE-START1
0.01% ( 2): FMT-CHAR
0.06% ( 18): FMT0
0.01% ( 3): FMT1
0.02% ( 6): PUSH-WARNING-FRAME
0.01% ( 2): POP-WARNING-FRAME
0.00% ( 1): WARNING-OFF-P
0.03% ( 9): ASCII-CODE!
0.01% ( 2): CHECK-SUM1
0.17% ( 48): CHECK-SUM-INC
0.04% ( 12): CHECK-SUM-STRING1
0.01% ( 2): CHECK-SUM-STRING2
0.08% ( 24): CHECK-SUM-OBJ1
0.01% ( 4): PROGRAM-TERMP
0.07% ( 19): GUARD
0.06% ( 16): CONS-TERM1
0.01% ( 2): CAR-CDR-NEST
0.00% ( 1): DUMB-NEGATE-LIT
0.02% ( 7): UNTRANSLATE1
0.00% ( 1): SET-CURRENT-PACKAGE
0.00% ( 1): SET-LD-PROMPT
0.00% ( 1): NEW-NAMEP
0.01% ( 2): SET-LD-ERROR-ACTION
0.02% ( 6): GLOBAL-SET
0.00% ( 1): LEGAL-CONSTANTP
0.00% ( 1): LEGAL-VARIABLEP
0.01% ( 2): LAMBDA-KEYWORDP
0.00% ( 1): ARGLISTP1
0.00% ( 1): EVISCERATE
0.02% ( 5): OUTPUT-IN-INFIXP
0.00% ( 1): MAX-WIDTH
0.01% ( 3): FMT-HARD-RIGHT-MARGIN
0.00% ( 1): FMT-SOFT-RIGHT-MARGIN
0.00% ( 1): PPR2-COLUMN
0.00% ( 1): SCAN-PAST-WHITESPACE
0.00% ( 1): DEFAULT-EVISC-TUPLE
0.00% ( 1): CHECK-SUM
0.00% ( 1): CHECK-SUM-NATURAL
0.02% ( 6): CHECK-SUM-STRING
0.01% ( 3): ARITY
0.01% ( 2): STOBJS-IN
0.11% ( 33): STOBJS-OUT
0.00% ( 1): ALL-NILS
0.01% ( 2): SYMBOL-CLASS
0.01% ( 3): COLLECT-NON-X
0.01% ( 2): ALL->=-LEN
0.00% ( 1): STRIP-CADRS
0.01% ( 2): DOUBLETON-LIST-P
0.02% ( 6): CONS-TERM
0.02% ( 7): SUBLIS-VAR
0.02% ( 5): SUBLIS-VAR-LST
0.01% ( 2): SUBCOR-VAR
0.00% ( 1): CONJOIN
0.00% ( 1): COND-LENGTH
0.00% ( 1): UNTRANSLATE-CONS
0.03% ( 8): PROOFS-CO
0.01% ( 4): CHK-PROOFS-CO
0.01% ( 2): LD-ERROR-TRIPLES
0.00% ( 1): CHK-LD-QUERY-CONTROL-ALIST
0.01% ( 3): PRINT-CHECKPOINTS
0.01% ( 3): TERMP
0.02% ( 5): CHK-LENGTH-AND-KEYS
0.04% ( 12): BIND-MACRO-ARGS-KEYS1
0.02% ( 5): BIND-MACRO-ARGS-OPTIONAL
0.07% ( 19): BIND-MACRO-ARGS1
0.03% ( 8): LATCH-STOBJS1
0.93% ( 268): RAW-EV-FNCALL
0.25% ( 73): TRANSLATED-ACL2-UNWIND-PROTECTP4
0.26% ( 75): EV-FNCALL-REC
0.89% ( 256): EV-REC
0.00% ( 1): EV-REC-ACL2-UNWIND-PROTECT
0.05% ( 14): EV-FNCALL
0.09% ( 26): EV
0.01% ( 4): UNTRANSLATE-LST
0.16% ( 45): MACROEXPAND1
0.01% ( 3): CHK-DCL-LST
0.01% ( 2): COLLECT-DECLARATIONS
0.01% ( 2): GENVAR
0.03% ( 10): TRANSLATE11-MV-LET
1.12% ( 323): TRANSLATE11
0.20% ( 58): TRANSLATE11-LST
0.08% ( 23): TRANSLATE1
0.07% ( 21): TRANS-EVAL
0.02% ( 5): KWOTE-LST
0.01% ( 4): MACRO-ARGS
0.01% ( 2): REMOVE-KEYWORD
0.01% ( 4): BIND-MACRO-ARGS-AFTER-REST
0.10% ( 28): BIND-MACRO-ARGS
0.07% ( 21): FIND-FIRST-NON-NIL
0.10% ( 29): LATCH-STOBJS
0.02% ( 5): TRANSLATED-ACL2-UNWIND-PROTECTP
0.02% ( 6): STOBJP
0.01% ( 3): ACL2-SYSTEM-NAMEP
0.06% ( 18): BIG-N
0.41% ( 117): EV-REC-LST
0.01% ( 2): UNTOUCHABLE-P
0.01% ( 3): COLLECT-DCLS
0.01% ( 2): NUMBER-OF-STRINGS
0.01% ( 3): REMOVE-STRINGS
0.00% ( 1): GET-STRING
0.00% ( 1): LISTIFY
0.00% ( 1): TRANSLATE-DECLARATION-TO-GUARD-VAR-LST
0.00% ( 1): IGNORE-VARS
0.01% ( 2): MV-NTH-LIST
0.09% ( 26): TRANSLATE-DEREF
0.00% ( 1): FIND-FIRST-VAR-LST
0.02% ( 5): COMPUTE-STOBJ-FLAGS
0.02% ( 5): COMPUTE-INCLP-LST1
0.01% ( 4): COMPUTE-INCLP-LST
0.01% ( 2): ALL-FNNAMES1
0.01% ( 2): TRANSLATE
0.03% ( 8): REPLACED-STOBJ
0.01% ( 2): REPLACE-STOBJS1
0.00% ( 1): REPLACE-STOBJS
0.01% ( 4): USER-STOBJSP
0.00% ( 1): CHK-USER-STOBJ-ALIST
0.01% ( 2): USER-STOBJ-ALIST-SAFE
0.20% ( 57): RULE-NAME-DESIGNATORP
0.02% ( 6): THEORYP!1
0.01% ( 4): CONVERT-THEORY-TO-UNORDERED-MAPPING-PAIRS1
0.00% ( 1): TYPE-SET-BINARY-*
0.01% ( 4): TYPE-SET-<-1
0.01% ( 3): TYPE-SET-<
0.01% ( 3): TYPE-SET-RECOGNIZER
0.01% ( 3): TYPE-SET-EQUAL
0.03% ( 8): TYPE-SET-QUOTE
0.10% ( 30): TERM-ORDER
2.39% ( 689): ONE-WAY-UNIFY1
1.28% ( 369): CANONICAL-REPRESENTATIVE
0.01% ( 2): SUBST-TYPE-ALIST1
0.01% ( 2): EXTEND-TYPE-ALIST
0.02% ( 6): ASSOC-EQUIV+
0.04% ( 11): ASSOC-TYPE-ALIST
0.00% ( 1): ANCESTORS-CHECK1
0.01% ( 3): TERM-AND-TYP-TO-LOOKUP
0.02% ( 6): PUSH-ACCP
0.01% ( 3): POP-ACCP
0.01% ( 3): ASSUME-TRUE-FALSE-<
0.08% ( 23): TYPE-SET
0.01% ( 2): TYPE-SET-RELIEVE-HYPS
0.03% ( 8): TYPE-SET-WITH-RULE
0.08% ( 23): TYPE-SET-PRIMITIVE
0.00% ( 1): ASSUME-TRUE-FALSE-IF
0.11% ( 32): ASSUME-TRUE-FALSE
0.00% ( 1): ASSUME-TRUE-FALSE1
0.01% ( 4): PROPER/IMPROPER-CONS-TS-TUPLE
0.00% ( 1): RETURN-TYPE-ALIST
0.00% ( 1): TYPE-ALIST-EQUALITY-LOOP1
0.01% ( 2): RECONSIDER-TYPE-ALIST
0.00% ( 1): EQUAL-X-CONS-X-YP
0.00% ( 1): NORMALIZE
0.00% ( 1): NORMALIZE-OR-DISTRIBUTE-FIRST-IF
0.01% ( 2): DISTRIBUTE-FIRST-IF
0.99% ( 286): ASSOC-EQUAL-CDR
0.36% ( 105): RUNEP
0.00% ( 1): FRUNIC-MAPPING-PAIR
0.01% ( 4): FN-RUNE-NUME
0.08% ( 22): GET-NEXT-NUME
0.01% ( 3): DEREF-MACRO-NAME
0.03% ( 8): RUNIC-THEORYP1
0.31% ( 89): FIND-MAPPING-PAIRS-TAIL1
0.43% ( 124): FIND-MAPPING-PAIRS-TAIL
0.06% ( 16): AUGMENT-RUNIC-THEORY1
0.01% ( 2): DUPLICITOUS-MERGE-CAR
0.04% ( 11): RUNIC-THEORY
0.36% ( 105): ENABLED-NUMEP
0.00% ( 1): ENABLED-RUNEP
0.00% ( 1): THEORY-WARNING-FNS
0.02% ( 6): RECOMPRESS-GLOBAL-ENABLED-STRUCTURE
0.01% ( 2): RECOMPRESS-STOBJ-ACCESSOR-ARRAYS
0.01% ( 3): PUFFERT
0.19% ( 54): MOST-RECENT-ENABLED-RECOG-TUPLE
0.00% ( 1): TYPE-SET-CAR
0.01% ( 3): VAR-FN-COUNT
0.01% ( 2): VAR-FN-COUNT-LST
0.02% ( 5): FN-COUNT-1
0.00% ( 1): FIND-RUNED-TYPE-PRESCRIPTION
0.01% ( 4): MV-ATF
0.01% ( 3): ASSUME-TRUE-FALSE-ERROR
0.05% ( 15): NON-CONS-CDR
0.89% ( 256): ONE-WAY-UNIFY1-LST
0.03% ( 10): ONE-WAY-UNIFY1-EQUAL1
0.05% ( 14): ONE-WAY-UNIFY1-EQUAL
0.04% ( 11): ONE-WAY-UNIFY
0.02% ( 5): SUBST-TYPE-ALIST
0.00% ( 1): INFECT-TYPE-ALIST-ENTRY
0.01% ( 4): EXTEND-TYPE-ALIST-SIMPLE
0.01% ( 3): EXTEND-TYPE-ALIST1
0.82% ( 235): ASSOC-EQUIV
0.01% ( 4): PUSH-ANCESTOR
0.01% ( 2): ANCESTORS-CHECK
0.00% ( 1): TYPE-SET-FINISH
0.02% ( 6): SEARCH-TYPE-ALIST
0.02% ( 5): FREE-VARSP
0.02% ( 5): FREE-VARSP-LST
0.00% ( 1): DELETE1-EQUAL
0.00% ( 1): MERGE-SORT-CAR->
0.02% ( 5): TYPE-SET-WITH-RULE1
0.04% ( 12): TYPE-SET-WITH-RULES
0.00% ( 1): EXTEND-WITH-PROPER/IMPROPER-CONS-TS-TUPLE
0.00% ( 1): OK-TO-FORCE-ENS
0.00% ( 1): TYPE-ALIST-CLAUSE-FINISH1
0.00% ( 1): KNOWN-WHETHER-NIL
0.00% ( 1): NORMALIZE-WITH-TYPE-SET
0.01% ( 2): NORMALIZE-LST
0.01% ( 3): ENS
0.00% ( 1): ADD-LITERAL
0.01% ( 2): FC-ACTIVATION
0.00% ( 1): ADD-NEW-FC-POTS
0.00% ( 1): MULT-RELIEVE-FC-HYPS
0.00% ( 1): MULT-ADVANCE-EACH-FC-ACTIVATION1
0.01% ( 2): MULT-ADVANCE-FC-ACTIVATION1
0.00% ( 1): MULT-ADVANCE-FC-ACTIVATION
0.01% ( 2): FCD-RUNEP
0.00% ( 1): SORT-APPROVED1-RATING1
0.00% ( 1): FORWARD-CHAIN
0.00% ( 1): REWRITE-ATM
0.00% ( 1): FIND-TRIVIAL-EQUIVALENCE1
0.00% ( 1): ADD-LITERAL-AND-PT
0.01% ( 2): BUILT-IN-CLAUSEP
0.01% ( 3): STRIP-NON-REWRITTENP-ASSUMPTIONS
0.01% ( 2): RESUME-SUSPENDED-ASSUMPTION-REWRITING1
0.02% ( 5): REWRITE-CLAUSE
0.00% ( 1): SIMPLIFY-CLAUSE1
0.01% ( 2): SIMPLIFY-CLAUSE
0.00% ( 1): PARSE-CLAUSE-ID1
0.00% ( 1): PARSE-CLAUSE-ID
0.00% ( 1): CONJOIN-CLAUSE-TO-CLAUSE-SET
0.00% ( 1): SOME-ELEMENT-MEMBER-COMPLEMENT-TERM
0.00% ( 1): SPLIT-ON-ASSUMPTIONS
0.01% ( 2): ADD-NEW-FC-POTS-LST
0.00% ( 1): ADD-NEW-FC-POTS-LST-LST
0.00% ( 1): MAKE-TTREES-FROM-FC-DERIVATIONS
0.00% ( 1): SCONS-TAG-TREES
0.01% ( 3): ADVANCE-FC-POT-LST
0.00% ( 1): TYPE-ALIST-FCD-LST
0.01% ( 3): MAX-LEVEL-NO
0.00% ( 1): MAX-LEVEL-NO-LST
0.00% ( 1): GET-LEVEL-NO
0.00% ( 1): REWRITE-CLAUSE-TYPE-ALIST
0.00% ( 1): TRIVIAL-CLAUSE-P
0.00% ( 1): ASSUMNOTE-LIST-TO-TOKEN-LIST
0.00% ( 1): RESUME-SUSPENDED-ASSUMPTION-REWRITING
0.00% ( 1): HELPFUL-LITTLE-ECNT-MSG
0.01% ( 2): REWRITE-CLAUSE-LST
0.00% ( 1): ENUMERATE-ELEMENTS
0.01% ( 4): PARSE-MATCH
0.00% ( 1): FFNNAMEP
0.02% ( 5): FFNNAMEP-HIDE
0.00% ( 1): IF-COMPILE
0.75% ( 216): IF-INTERP-ASSUMED-VALUE2
0.02% ( 6): IF-INTERP
0.01% ( 2): SPLICE-INSTRS1
0.00% ( 1): SUBSUMPTION-REPLACEMENT-LOOP
0.01% ( 3): OBJ-TABLE
0.02% ( 6): REWRITE-SOLIDIFY
0.00% ( 1): REWRITE-IF1
0.01% ( 3): EQUAL-MOD-ALIST
0.00% ( 1): SEARCH-GROUND-UNITS1
0.02% ( 5): COUNT-IFS
0.01% ( 2): OK-TO-FORCE
0.00% ( 1): RESTORE-BRR-GLOBALS
0.01% ( 2): SAVE-BRR-GLOBALS
0.01% ( 4): INITIALIZE-BRR-STACK
0.01% ( 4): BRKPT1
0.01% ( 3): BRKPT2
0.01% ( 3): EXPAND-PERMISSION-P
0.00% ( 1): EV-FNCALL-META
0.01% ( 2): EV-SYNP
0.01% ( 4): FLATTEN-ANDS-IN-LIT
0.00% ( 1): NTH-UPDATE-REWRITER-TARGETP
0.00% ( 1): RDEPTH-ERROR
0.15% ( 42): REWRITE
0.01% ( 2): REWRITE-IF
0.08% ( 22): RELIEVE-HYP
0.05% ( 15): RELIEVE-HYPS1
3.42% ( 984): REWRITE-WITH-LEMMA
1.71% ( 493): REWRITE-WITH-LEMMAS1
0.01% ( 3): REWRITE-FNCALL
0.04% ( 11): REWRITE-WITH-LEMMAS
0.01% ( 2): ADD-POLYS-AND-LEMMAS2-NL
0.04% ( 12): GENEQV-REFINEMENTP1
0.05% ( 15): GENEQV-REFINEMENTP
0.03% ( 9): SOME-CONGRUENCE-RULE-DISABLEDP
0.01% ( 4): GENEQV-LST
0.01% ( 2): SUBST-EXPR1-LST
0.00% ( 1): SUBST-EXPR
0.00% ( 1): IF-INTERP-ASSUMED-VALUE
0.00% ( 1): IF-INTERP-ADD-CLAUSE
0.00% ( 1): MERGE-SORT-LENGTH
0.04% ( 11): FIND-REWRITING-EQUIVALENCE
0.00% ( 1): REWRITE-IF11
0.01% ( 3): NOT-TO-BE-REWRITTENP
0.00% ( 1): INVISIBLE-FNS
0.00% ( 1): LOOP-STOPPERP-REC
0.01% ( 2): IF-TAUTOLOGYP
0.02% ( 7): BEING-OPENEDP-REC
0.00% ( 1): RECURSIVE-FN-ON-FNSTACKP
0.00% ( 1): TOO-MANY-IFS
0.00% ( 1): RESTORE-BRR-GLOBALS1
0.01% ( 2): FREE-P
0.04% ( 12): ONE-WAY-UNIFY-RESTRICTIONS1
0.09% ( 25): ONE-WAY-UNIFY-RESTRICTIONS
0.00% ( 1): NTH-UPDATE-REWRITER-TARGET-LSTP
0.01% ( 3): LAMBDA-NEST-HIDEP
0.05% ( 13): REWRITE-ARGS
0.01% ( 2): REWRITE-PRIMITIVE
0.00% ( 1): ADD-POLYS-AND-LEMMAS1
0.00% ( 1): ADD-POLYS-AND-LEMMAS
0.00% ( 1): ADD-TERMS-AND-LEMMAS
0.01% ( 2): LOAD-HINT-SETTINGS-INTO-RCNST
0.00% ( 1): UPDATE-HINT-SETTINGS
0.00% ( 1): REMOVE-TRIVIAL-CLAUSES
0.01% ( 2): MAKE-EVENT-TUPLE
0.10% ( 30): SCAN-TO-LANDMARK-NUMBER
0.00% ( 1): UPDATE-WORLD-INDEX
0.00% ( 1): PRINT-REDEFINITION-WARNING
0.03% ( 10): INITIALIZE-SUMMARY-ACCUMULATORS
0.02% ( 5): PRINT-SUMMARY
0.00% ( 1): WITH-CTX-SUMMARIZED
0.04% ( 12): INSTALL-EVENT
0.00% ( 1): STOP-REDUNDANT-EVENT
0.03% ( 8): CHK-ALL-BUT-NEW-NAME
0.00% ( 1): CHK-BOOT-STRAP-REDEFINEABLE-NAMEP
0.02% ( 5): CHK-JUST-NEW-NAME
0.01% ( 3): CHK-WELL-FORMED-DOC-STRING
0.01% ( 2): CHK-ARGLIST
0.00% ( 1): CHK-DEFUNS-TUPLES
0.02% ( 7): GET-GUARDS1
0.01% ( 3): GET-MEASURES1
0.01% ( 4): GET-UNAMBIGUOUS-XARGS-FLG1/EDCLS
0.00% ( 1): CHK-FREE-AND-IGNORED-VARS
0.00% ( 1): TRANSLATE-EXPAND-HINT1
0.00% ( 1): TRANSLATE-EXPAND-HINT
0.00% ( 1): CHK-DO-NOT-EXPR-VALUE
0.01% ( 2): CONTAINS-GUARD-HOLDERSP
0.00% ( 1): TRANSLATE-HINT-SETTINGS
0.01% ( 3): TRANSLATE-HINT
0.00% ( 1): TRANSLATE-HINTS
0.00% ( 1): ACCESS-COMMAND-TUPLE-FORM
0.00% ( 1): ACCESS-EVENT-TUPLE-NUMBER
0.00% ( 1): MAX-ABSOLUTE-EVENT-NUMBER
0.00% ( 1): NEXT-ABSOLUTE-EVENT-NUMBER
0.00% ( 1): SCAN-TO-COMMAND
0.01% ( 3): STORE-ABSOLUTE-EVENT-NUMBER
0.01% ( 4): THE-NAMEX-SYMBOL-CLASS
0.02% ( 5): ADD-EVENT-LANDMARK
0.01% ( 3): PROVED-FUNCTIONAL-INSTANCES-FROM-TAGGED-OBJECTS
0.01% ( 2): CHK-VIRGIN
0.00% ( 1): TRANSLATE-DOC
0.01% ( 3): UPDATE-DOC-DATA-BASE
0.00% ( 1): GET-MEASURES2
0.01% ( 4): GET-UNAMBIGUOUS-XARGS-FLG1
0.01% ( 3): CHK-FREE-VARS
0.00% ( 1): CHK-DECLARED-IGNORES
0.01% ( 2): TRANSLATE-TERM-LST
0.00% ( 1): COERCE-TO-ACL2-PACKAGE-LST
0.00% ( 1): CONVERT-TYPE-PRESCRIPTION-TO-TERM
0.02% ( 7): MERGE-SYMBOL-<
0.00% ( 1): GETPROP-X-LST
0.01% ( 4): TRANSLATE-BDD-HINT
0.01% ( 3): FIND-ABBREVIATION-LEMMA
0.01% ( 2): EXPAND-ABBREVIATIONS
0.01% ( 2): AND-ORP
0.01% ( 4): FIND-AND-OR-LEMMA
0.01% ( 2): EXPAND-AND-OR
0.00% ( 1): CLAUSIFY-INPUT1
0.00% ( 1): NO-OP-HISTP
0.01% ( 2): EXPAND-ANY-FINAL-IMPLIES1
0.00% ( 1): PREPROCESS-CLAUSE-MSG1
0.01% ( 2): DELETE-ASSUMPTIONS-1
0.01% ( 4): WATERFALL-MSG
0.01% ( 2): SET-CL-IDS-OF-ASSUMPTIONS
0.01% ( 2): COLLECT-ASSUMPTIONS
0.00% ( 1): DUMB-KEEP-ASSUMPTIONS-WITH-WEAKEST-TYPE-ALISTS
0.01% ( 2): EXTRACT-AND-CLAUSIFY-ASSUMPTIONS
0.01% ( 2): WATERFALL-STEP
0.01% ( 2): THANKS-FOR-THE-HINT
0.01% ( 2): WATERFALL0-WITH-HINT-SETTINGS
0.01% ( 2): WATERFALL0
0.02% ( 5): WATERFALL1-LST
0.00% ( 1): WATERFALL
0.00% ( 1): POP-CLAUSE-MSG
0.00% ( 1): PROCESS-ASSUMPTIONS-MSG
0.01% ( 2): PROCESS-ASSUMPTIONS
0.01% ( 3): PROVE-LOOP1
0.01% ( 3): PROVE-LOOP
0.01% ( 2): MAKE-PSPV
0.00% ( 1): CHK-ASSUMPTION-FREE-TTREE
0.02% ( 6): PROVE
0.01% ( 2): ALL-VARS-BAG
0.01% ( 2): DELETE-ASSUMPTIONS
0.00% ( 1): PUT-TTREE-INTO-PSPV
0.01% ( 2): DUMB-TYPE-ALIST-IMPLICATIONP
0.00% ( 1): PARTITION-ACCORDING-TO-ASSUMPTION-TERM
0.00% ( 1): DUMB-ASSUMPTION-SUBSUMPTION
0.01% ( 2): MAYBE-WARN-FOR-USE-HINT
0.01% ( 2): MAYBE-WARN-ABOUT-THEORY-FROM-RCNSTS
0.01% ( 2): WATERFALL1
0.00% ( 1): QUICKLY-COUNT-ASSUMPTIONS
0.01% ( 2): PC-PROMPT-FN
0.00% ( 1): MAKE-OFFICIAL-PC-INSTR
0.00% ( 1): CHECK-FORMALS-LENGTH
0.01% ( 2): PRINT-PC-PROMPT
0.01% ( 2): PC-MACROEXPAND
0.01% ( 4): MAYBE-PRINT-PROVED-GOAL-MESSAGE
0.00% ( 1): PC-PROCESS-ASSUMPTIONS
0.06% ( 16): PC-SINGLE-STEP-PRIMITIVE
0.00% ( 1): PC-SINGLE-STEP-1
0.01% ( 2): PC-SINGLE-STEP
0.02% ( 5): PC-MAIN-LOOP
0.00% ( 1): PROOF-CHECKER
0.01% ( 2): MAKE-PRETTY-PC-INSTR
0.00% ( 1): CL-SET-TO-IMPLICATIONS
0.00% ( 1): MAKE-PC-ENS
0.01% ( 2): INITIAL-RCNST-FROM-ENS
0.01% ( 2): UNPRETTYIFY
0.02% ( 5): INTERPRET-TERM-AS-REWRITE-RULE
0.01% ( 2): PUT-MATCH-FREE-VALUE
0.00% ( 1): FREE-VARS-IN-HYPS-CONSIDERING-BIND-FREE
0.01% ( 3): CREATE-REWRITE-RULE
0.01% ( 2): FIND-SUBSUMED-RULE-NAMES
0.00% ( 1): FIND-SUBSUMING-RULE-NAMES
0.01% ( 4): CHK-REWRITE-RULE-WARNINGS
0.01% ( 4): CHK-ACCEPTABLE-REWRITE-RULE2
0.00% ( 1): CHK-LEGAL-LINEAR-TRIGGER-TERMS
0.02% ( 7): TRANSLATE-RULE-CLASS-ALIST
0.01% ( 3): TRANSLATE-RULE-CLASS1
0.01% ( 3): REASON-FOR-NON-KEYWORD-VALUE-LISTP
0.01% ( 2): TRANSLATE-RULE-CLASSES1
0.00% ( 1): CHK-ACCEPTABLE-X-RULE
0.01% ( 2): CHK-ACCEPTABLE-RULES
0.00% ( 1): ADD-X-RULE
0.00% ( 1): PROVE-COROLLARIES
0.02% ( 5): PRINT-RULE-STORAGE-DEPENDENCIES
0.05% ( 14): DEFTHM-FN1
0.01% ( 2): UNPRETTYIFY/ADD-HYPS-TO-PAIRS
0.01% ( 3): REMOVE-LAMBDAS
0.01% ( 3): REMOVE-LAMBDAS-LST
0.00% ( 1): HIDE-LAMBDAS
0.00% ( 1): LOOP-STOPPER1
0.00% ( 1): FREE-VARS-IN-FC-HYPS
0.00% ( 1): BAD-SYNP-HYP-MSG
0.00% ( 1): CHK-ACCEPTABLE-REWRITE-RULE
0.01% ( 2): ADD-REWRITE-RULE2
0.01% ( 2): ADD-REWRITE-RULE
0.00% ( 1): DESTRUCTURE-FORWARD-CHAINING-TERM
0.01% ( 2): ADD-TYPE-SET-INVERTER-RULE
0.00% ( 1): CHK-PRIMITIVE-INSTRUCTION-LISTP
0.01% ( 2): TRANSLATE-RULE-CLASSES
0.01% ( 2): TRUNCATE-CLASS-ALIST
0.00% ( 1): MAKE-RUNES1
0.01% ( 2): MAKE-RUNIC-MAPPING-PAIRS
0.01% ( 2): NON-TAUTOLOGICAL-CLASSES
0.41% ( 118): ASSOC-EQ-EQ
0.00% ( 1): WARN-ON-INAPPROPRIATE-DEFUN-MODE
0.01% ( 2): DEFTHM-FN
0.00% ( 1): CHK-EXTENSIBLE-RULE-CLASSES
0.01% ( 4): ALL-CALLS
0.00% ( 1): TERMINATION-MACHINE
0.01% ( 2): GUESS-MEASURE-ALIST
0.00% ( 1): DESTRUCTURE-DEFINITION
0.00% ( 1): ADD-DEFINITION-RULE
0.01% ( 3): TYPE-SET-AND-RETURNED-FORMALS-WITH-RULE
0.01% ( 2): TYPE-SET-AND-RETURNED-FORMALS-WITH-RULES
0.05% ( 13): TYPE-SET-AND-RETURNED-FORMALS
0.00% ( 1): GUESS-TYPE-PRESCRIPTION-FOR-FN-STEP
0.00% ( 1): CLEANSE-TYPE-PRESCRIPTIONS
0.01% ( 2): PRIMITIVE-RECURSIVE-ARGP
0.00% ( 1): EXPAND-CLIQUE-ALIST-TERM
0.01% ( 4): TRANSLATE-BODIES1
0.00% ( 1): TERMINATION-MACHINES
0.00% ( 1): PREPROCESS-HYP
0.01% ( 3): PREPROCESS-HYPS
0.01% ( 4): PUTPROP-BODY-LST
0.00% ( 1): TYPE-SET-AND-RETURNED-FORMALS-WITH-RULE1
0.01% ( 2): MAKE-CONTROLLER-POCKET
0.01% ( 2): SUPER-DEFUN-WART-BINDINGS
0.01% ( 2): GET-IGNORES
0.00% ( 1): RELEVANT-SLOTS-TERM
0.00% ( 1): MACRO-VARS
0.00% ( 1): CHK-MACRO-ARGLIST1
0.00% ( 1): CHK-DEFMACRO-WIDTH
0.01% ( 3): DEFMACRO-FN
0.14% ( 40): SET-DIFFERENCE-AUGMENTED-THEORIES-FN1
0.01% ( 3): FUNCTION-THEORY-FN1
0.07% ( 21): CURRENT-THEORY1
0.00% ( 1): IN-ARITHMETIC-THEORY-FN
0.01% ( 2): CHK-TABLE-GUARD
0.03% ( 9): TABLE-FN1
0.00% ( 1): NAME-INTRODUCED
0.06% ( 16): CHK-EMBEDDED-EVENT-FORM
0.09% ( 26): EVAL-EVENT-LST
0.00% ( 1): DEFINITIONAL-CONSTRAINTS
0.02% ( 5): COLLECT-IDEAL-USER-DEFUNS1
0.00% ( 1): CHK-PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS
0.02% ( 6): REV-STRIP-CDRS
0.01% ( 3): APPEND-STRIP-CDRS
0.27% ( 79): REVAPPEND-DELETE-RUNES-BASED-ON-SYMBOLS
0.01% ( 3): PUT-ASSOC-EQUAL-FAST
0.04% ( 12): NEW-TRIPS
0.01% ( 2): PRINT-PROMPT
0.03% ( 8): CHK-ACCEPTABLE-LD-FN1-PAIR
0.00% ( 1): CLOSE-CHANNELS
0.01% ( 2): CHK-ACCEPTABLE-LD-FN
0.02% ( 6): F-PUT-LD-SPECIALS
0.01% ( 3): F-GET-LD-SPECIALS
0.00% ( 1): LD-READ-COMMAND
0.00% ( 1): LD-PRINT-COMMAND
0.01% ( 4): LD-READ-EVAL-PRINT
0.00% ( 1): LD-FN
0.01% ( 3): MFC-AP
0.00% ( 1): STOBJ-ALIST
0.00% ( 1): ACL2_*1*_ACL2::BINARY-+
0.00% ( 1): ACL2_*1*_ACL2::UNARY--
0.01% ( 3): ACL2_*1*_COMMON-LISP::<
0.01% ( 3): ACL2_*1*_COMMON-LISP::CAR
0.01% ( 2): ACL2_*1*_COMMON-LISP::CDR
0.00% ( 1): ACL2_*1*_COMMON-LISP::SYMBOL-NAME
0.06% ( 17): ONEIFY
0.00% ( 1): ONEIFY-CLTL-CODE-PROGRAM
0.00% ( 1): ONEIFY-CLTL-CODE
0.01% ( 4): MAYBE-POP-UNDO-STACK
0.22% ( 63): ADD-TRIP
0.10% ( 28): UNDO-TRIP
0.01% ( 2): FLUSH-TRIP
0.13% ( 37): EXTEND-WORLD1
0.05% ( 15): RETRACT-WORLD1
0.00% ( 1): RECOVER-WORLD
0.00% ( 1): VIRGINP
0.01% ( 3): CHK-VIRGIN2
0.04% ( 11): ACL2_*1*_ACL2::COMPLEX-RATIONALP
0.04% ( 11): ACL2_*1*_COMMON-LISP::CONS
0.00% ( 1): ACL2_*1*_COMMON-LISP::CONSP
0.00% ( 1): ACL2_*1*_COMMON-LISP::SYMBOLP
0.02% ( 5): ONEIFY-LST
0.02% ( 6): KEY-LESSEQP
0.02% ( 5): MERGE-INTO-ALIST
0.22% ( 63): DESTRUCTIVE-PUSH-ASSOC
0.21% ( 61): DESTRUCTIVE-POP-ASSOC
0.01% ( 3): CHECK-ACL2-WORLD-INVARIANT
0.00% ( 1): STOBJ-PRINT-SYMBOL
0.01% ( 2): PROMOTE-GUTS
0.01% ( 3): ACL2-PC::PROMOTE
0.00% ( 1): CHK-?S
0.00% ( 1): ACL2-PC::DIVE
0.00% ( 1): ACL2-PC::SHOW-ABBREVIATIONS
0.00% ( 1): EXPAND-ADDRESS
0.01% ( 2): ACL2-PC::DV
0.00% ( 1): DEPOSIT-TERM-IN-GOAL
0.01% ( 2): ACL2-PC::SEQUENCE
0.00% ( 1): ACL2-PC::PROTECT
0.00% ( 1): ACL2-PC::NX
0.01% ( 2): ACL2-PC::S
0.01% ( 2): ACL2-PC::EXPAND
0.00% ( 1): PAIR-KEYWORDS
0.01% ( 2): ACL2_*1*_ACL2::LD-SKIP-PROOFSP
0.00% ( 1): ACL2_*1*_ACL2::STATE-GLOBAL-LET*-CLEANUP
0.00% ( 1): ACL2_*1*_ACL2::STATE-GLOBAL-LET*-GET-GLOBALS
0.01% ( 2): ACL2_*1*_ACL2::PUT-GLOBAL
0.00% ( 1): ACL2_*1*_ACL2::DELETE-PAIR
0.00% ( 1): ACL2_*1*_ACL2::MV-NTH
0.01% ( 2): ACL2_*1*_ACL2::FUNCTION-SYMBOLP
0.00% ( 1): ACL2_*1*_COMMON-LISP::LAST
0.00% ( 1): ACL2_*1*_COMMON-LISP::EXPT
0.00% ( 1): ACL2_*1*_ACL2::XXXJOIN
0.01% ( 2): ACL2_*1*_ACL2::INTERSECTP-EQUAL
0.01% ( 2): ACL2_*1*_ACL2::INTERSECTP-EQ
0.01% ( 2): ACL2_*1*_ACL2::STRING-APPEND-LST
0.01% ( 4): ACL2_*1*_ACL2::BINARY-APPEND
0.00% ( 1): ACL2_*1*_ACL2::SUBSETP-EQ
0.01% ( 3): ACL2_*1*_ACL2::COND-MACRO
0.01% ( 3): ACL2_*1*_COMMON-LISP::LENGTH
0.01% ( 4): ACL2_*1*_COMMON-LISP::ENDP
0.01% ( 3): ACL2_*1*_COMMON-LISP::EQ
0.00% ( 1): ACL2_*1*_ACL2::SIGNED-BYTE-P
0.00% ( 1): ACL2_*1*_ACL2::BUILD-STATE1
0.00% ( 1): ACL2_*1*_ACL2::KWOTE
0.00% ( 1): ACL2_*1*_ACL2::QUOTEP
0.00% ( 1): ACL2_*1*_ACL2::SYMBOL-LISTP
0.00% ( 1): ACL2_*1*_ACL2::COND-CLAUSESP
0.00% ( 1): ACL2_*1*_ACL2::OR-MACRO
0.01% ( 3): ACL2_*1*_ACL2::AND-MACRO
0.00% ( 1): ACL2_*1*_ACL2::LIST-MACRO
0.00% ( 1): ACL2_*1*_ACL2::TRUE-LISTP
0.00% ( 1): ACL2_*1*_COMMON-LISP::NOT
0.10% ( 30): ACL2_*1*_ACL2::IMPLIES
Total ticks 28774
134519984
ACL2>5262.780u 14.330s 1:28:26.69 99.4% 0+0k 0+0io 5157pf+0w
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- Matt
cc: address@hidden
From: "Camm Maguire" <address@hidden>
Date: 12 Aug 2003 08:17:55 -0400
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
X-WSS-ID: 1326057C589000-01-01
Content-Type: text/plain;
charset=us-ascii
Greetings! If I understand you right, you should not have to. The
patch only affects the building of the "raw" image, i.e. when first
running a binary produced by the system's linker 'ld'. I've forgotten
a bit how acl2 produces its binary, but if memory serves, you never
call ld, but just pipe lisp commands to saved_gcl, including
compile-file, load, and save-system, and then use the resulting
image. In this case, the patch is alrady effective by the time
saved_gcl is produced, and hence anything that it dumps.
The Debian acl2 package (a new version of which should be forthcoming
soon to address some of your old concerns) builds the acl2 image using
the alternate method provided by the function '(compiler::link ...' in
order to be able to ship acl2 for 5 less common Debian platforms. In
such a case, the patch needs to be in at the point of executing
compiler::link.
Take care,
"Matt Kaufmann" <address@hidden> writes:
> Camm --
>
> Do I need to rebuild all existing .o files that are loaded as (a
preliminary)
> part of the test, before I run the test after rebuilding GCL and then ACL2?
>
> -- Matt
> cc: address@hidden
> From: "Camm Maguire" <address@hidden>
> Date: 11 Aug 2003 21:38:04 -0400
> User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> X-WSS-ID: 13269B74500212-01-01
> Content-Type: text/plain;
> charset=us-ascii
>
> Greetings!
>
> OK, I suppose you may know of something that needed changing in your
> environment, but I retraced your steps, and there is a problem with
> our count of the symbols in the bfd symbol table. I think you will
> need this patch, now committed into 2.5.4:
>
>
=============================================================================
> Index: fat_string.c
> ===================================================================
> RCS file: /cvsroot/gcl/gcl/o/fat_string.c,v
> retrieving revision 1.14.4.1
> diff -u -r1.14.4.1 fat_string.c
> --- fat_string.c 4 Aug 2003 23:38:51 -0000 1.14.4.1
> +++ fat_string.c 12 Aug 2003 01:30:57 -0000
> @@ -222,6 +222,8 @@
>
> #if defined(HAVE_LIBBFD) && ! defined(SPECIAL_RSYM)
>
> +static int bfd_update;
> +
> static MY_BFD_BOOLEAN
> bfd_combined_table_update(struct bfd_link_hash_entry *h,PTR ct) {
>
> @@ -236,9 +238,14 @@
> return MY_BFD_FALSE;
> }
>
> -
SYM_ADDRESS(combined_table,combined_table.length)=h->u.def.value+h->u.def.section->vma;
> - SYM_STRING(combined_table,combined_table.length)=(char
*)h->root.string;
> -
> + if (bfd_update) {
> + if (combined_table.length>=combined_table.alloc_length)
> + FEerror("combined table overflow", 0);
> +
> +
SYM_ADDRESS(combined_table,combined_table.length)=h->u.def.value+h->u.def.section->vma;
> + SYM_STRING(combined_table,combined_table.length)=(char
*)h->root.string;
> + }
> +
> combined_table.length++;
>
> return MY_BFD_TRUE;
> @@ -288,12 +295,17 @@
> #if defined(HAVE_LIBBFD)
> if (link_info.hash) {
>
> - if (combined_table.length+link_info.hash->table.size >=
> - combined_table.alloc_length)
> -
cfuns_to_combined_table(combined_table.length+link_info.hash->table.size+20);
> + bfd_update=0;
> + bfd_link_hash_traverse(link_info.hash,
> +
bfd_combined_table_update,&combined_table);
> +
> + if (combined_table.length >=combined_table.alloc_length)
> + cfuns_to_combined_table(combined_table.length);
>
> + bfd_update=1;
> bfd_link_hash_traverse(link_info.hash,
> bfd_combined_table_update,&combined_table);
> + bfd_update=0;
>
> }
> #endif
>
=============================================================================
>
> Other than this, you are invoking the profiler commands just right so
> far. If you have suggestions for better usability, e.g. _init
> address, etc., I'd like to hear them.
>
> Also coming soon -- gprof support. More later.
>
> Take care,
>
> "Matt Kaufmann" <address@hidden> writes:
>
> > Camm --
> >
> > OOPS -- my apologies! I just noticed that the environment had
changed when I
> > ran the test below, and I need to do some recompilation. So never
mind about
> > the error, although I'm still interested in whether I called the
> > profiling-related functions correctly.
> >
> > Thanks --
> > -- Matt
> > From: Matt Kaufmann <address@hidden>
> > Subject: Re: [Gcl-devel] Re: Profiling [ was Re: lisp reader
enhancement
> > To: address@hidden
> > CC: address@hidden
> > Date: 11 Aug 2003 15:02:46 -0500
> >
> > Hi, Camm --
> >
> > After rebuilding ACL2 on GCL,
> >
> > OK, we've rebuilt GCL, including (I believe) all patches you've sent,
and I've
> > built ACL2 on top of it and tried the test again. But I got an
error, as
> > explained below. Below I'll tell you what I did and then what the
error was.
> >
> > You said the following:
> >
> > b) run si::prof with the starting address you desire to
> > examine, and a 'scale' parameter indicating how many counter
> > profile array elements to allocate to each 256 bytes of code.
> > You can see these addresses reported on loading binary
> > modules, or you could use the DBEGIN value issued at configure
> > time. You could also try function-address. We need to make
> > it easier to just say 'profile my whole program', but what I
> > did was find the address of _init in gdb, find the value of
> > heap_end in gdb, figure out a good scale for this amount of
> > memory to correspond to a 1000000 byte array, and issue the
> > following call for maxima:
> >
> > :lisp (si::prof 134522412 15)
> >
> > I did the following, which seemed to give me _init and heap_end:
> >
> > [ 202 ] --> gdb gcl-saved_acl2
> > GNU gdb 5.3
> > Copyright 2002 Free Software Foundation, Inc.
> > GDB is free software, covered by the GNU General Public License,
and you are
> > welcome to change it and/or distribute copies of it under certain
conditions.
> > Type "show copying" to see the conditions.
> > There is absolutely no warranty for GDB. Type "show warranty" for
details.
> > This GDB was configured as "i686-pc-linux-gnu"...
> > (gdb) p _init
> > $1 = {<text variable, no debug info>} 0x8049cb0 <_init>
> > (gdb) p heap_end
> > $2 = 154292224
> > (gdb)
> >
> > I think you're saying that the second argument to si::prof should be
computed
> > as shown below:
> >
> > >(/ (- 154292224 #x8049cb0) 1000000.0)
> > ;heap_end ;_init
> > 19.77224
> >
> > So I did this:
> >
> > (si::set-up-profile 1000000 8000) ; ACL2 has about 4100 defuns and
about 600 macros
> > (si::prof #x8049cb0 20)
> >
> > After executing the forms above before starting on the "real"
computation, I
> > ran into this problem, which I don't think I've seen before:
> >
> > %%AND-TREE
> > [SGC for 3000 CONS pages..(10580 writable)..(T=19).GC finished]
> > [SGC for 3000 CONS pages..(10609 writable)..(T=19).GC finished]
> > [SGC for 3000 CONS pages..(10624 writable)..(T=20).GC finished]
> > [SGC for 232 FIXNUM pages..(10625 writable)..(T=22).GC finished]
> > [SGC for 232 FIXNUM pages..(10626 writable)..(T=22).GC finished]
> > [SGC for 232 FIXNUM pages..(10627 writable)..(T=21).GC finished]
> > [SGC for 3000 CONS pages..(10632 writable)..(T=21).GC finished]
> > [SGC off][GC for 750 RELOCATABLE-BLOCKS pages..(T=66).GC finished]
> > [SGC on][SGC off][GC for 750 RELOCATABLE-BLOCKS pages..(T=70).GC
finished]
> > [SGC on][SGC off][GC for 750 RELOCATABLE-BLOCKS pages..(T=73).GC
finished]
> > [SGC on][SGC for 3043 CONS pages..(7025 writable)..(T=11).GC
finished]
> > [SGC for 0 RELOCATABLE-BLOCKS pages..(7091 writable)..(T=10).GC
finished]
> > [SGC for 3043 CONS pages..(7820 writable)..(T=13).GC finished]
> >
> > Error: Frame stack overflow.
> > Fast links are on: do (si::use-fast-links nil) for debugging
> > Error signalled by IF.
> > Broken at COND. Type :H for Help.
> > ACL2>>
> >
> > Any suggestions?
> >
> > - -- Matt
> > cc: address@hidden, address@hidden
> > From: "Camm Maguire" <address@hidden>
> > Date: 05 Aug 2003 16:22:12 -0400
> > User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> > X-WSS-ID: 132ECD8D9243291-01-01
> > Content-Type: text/plain;
> > charset=us-ascii
> >
> > Hi Matt!
> >
> > "Matt Kaufmann" <address@hidden> writes:
> >
> > > Hi, Camm --
> > >
> > > I haven't yet rebuilt GCL since your last patch related to
profiling --
> > > actually Rob Sumners has been doing the builds so I'm waiting on
him (and he
> > > has a lot on his plate at work, though I imagine he may have
time soon).
> > >
> >
> > OK, please keep me posted. I might accept a small performance hit,
> > but not 3x :-).
> >
> > > But, I wanted to let you know I've discovered a bug in the
previous reader
> > > patches that you sent. It's illustrated below (comments added).
The problem
> > > goes away if (a . b) is replaced by (a b), so I guess this has
to do with
> > > reading dotted pairs.
> > >
> >
> > Here is a fix, just checked in:
> >
> > ===================================================================
> > RCS file: /cvsroot/gcl/gcl/o/read.d,v
> > retrieving revision 1.17
> > diff -u -r1.17 read.d
> > --- read.d 30 Jul 2003 20:26:01 -0000 1.17
> > +++ read.d 5 Aug 2003 20:18:10 -0000
> > @@ -663,6 +663,9 @@
> > c = read_char(in);
> > if (char_code(c) != ')')
> > FEerror("A dot appeared before a right parenthesis.", 0);
> > + else if (PP0>P0) PP0--; /* should be the only
other place
> > + outside of
read_object where
> > + closing parens are
read */
> > goto ENDUP;
> > }
> > vs_push(x);
> >
> >
> > Take care,
> >
> > > GCL (GNU Common Lisp) (2.5.3) Mon Jul 21 10:41:19 CDT 2003
> > > Licensed under GNU Library General Public License
> > > Dedicated to the memory of W. Schelter
> > >
> > > Use (help) to get some basic information on how to use GCL.
> > >
> > > >(make-package "ABC" :use nil)
> > >
> > > #<"ABC" package>
> > >
> > > >(import '(package-name symbol-package) (find-package "ABC"))
> > >
> > > T
> > >
> > > >(package-name (symbol-package 'xxxx))
> > >
> > > "USER"
> > >
> > > >*package*
> > >
> > > #<"USER" package>
> > >
> > > >'abc::((a . b))
> > >
> > > ((ABC::A . ABC::B))
> > >
> > > >(package-name (symbol-package 'xxxx)) ;;; !!! Here is the
first surprise.
> > >
> > > "ABC"
> > >
> > > >user::*package* ;;; !!! It's a little surprising that the
*package* is still
> > > ;;; right, even though the reader isn't using
that
> > > ;;; package.
> > >
> > > #<"USER" package>
> > >
> > > >
> > >
> > > -- Matt
> > > Resent-From: address@hidden
> > > Resent-To: address@hidden
> > > cc: address@hidden
> > > From: "Camm Maguire" <address@hidden>
> > > Date: 04 Aug 2003 19:21:07 -0400
> > > User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> > > X-WSS-ID: 133121B59149313-01-01
> > > Content-Type: text/plain;
> > > charset=us-ascii
> > >
> > > Greetings! Just a followup note here in case you're still
interested in
> > > trying to analyze the performance.
> > >
> > > 1) If you reran with the new gbc-time, I'd be interested to
know
> > > what it was.
> > >
> > > 2) I've been looking at GCL's two profiling modes. The first
is based
> > > on the 'profil' call to libc. It works, but unfortunately
our
> > > documentation is misleading/wrong. The idea is to:
> > >
> > > 0) Apply the following two patches:
> > >
> > >
===================================================================
> > > RCS file: /cvsroot/gcl/gcl/o/fat_string.c,v
> > > retrieving revision 1.14
> > > diff -u -r1.14 fat_string.c
> > > --- fat_string.c 15 Feb 2003 00:38:28 -0000 1.14
> > > +++ fat_string.c 4 Aug 2003 22:52:09 -0000
> > > @@ -49,7 +49,7 @@
> > > if( type_of(start_address)!=t_fixnum ||
type_of(scale)!=t_fixnum)
> > > FEerror("Needs start address and scale as args",0);
> > >
> > > - profil((void *) (ar->ust.ust_self), (ar->ust.ust_dim),
> > > + profil(!(fix(start_address)*fix(scale)) ? NULL : (void *)
(ar->ust.ust_self), (ar->ust.ust_dim),
> > > fix(start_address),fix(scale) << 8);
> > > RETURN1(start_address);
> > > }
> > > --- ptable.h 12 Jul 2002 22:00:48 -0000 1.4
> > > +++ ptable.h 4 Aug 2003 22:51:56 -0000
> > > @@ -50,7 +50,7 @@
> > > #ifdef SPECIAL_RSYM
> > > struct string_address_table c_table;
> > > #else
> > > -static struct bfd_link_info link_info;
> > > +struct bfd_link_info link_info;
> > > #endif
> > > struct string_address_table combined_table;
> > >
> > >
> > > a) in your program, first run set-up-profile, defined in
> > > profile.lsp (should be in your gcl autoload path). The first
> > > argument is the size of the profile array, with 1000000 being
> > > suggested in the docs -- this works for me. What is not
> > > documented is the optional second argument specifying the
> > > maximum number of functions in your image. I had to supply
> > > this to increase the default value when testing in maxima.
> > > Here is my call:
> > >
> > > :lisp (si::set-up-profile 1000000 8000)
> > >
> > >
> > > Loaded c and other function addresses
> > > Using profile-array length 1000000
> > > Use (si::prof 0 90) to start and (prof 0 0)
to stop:
> > > This starts monitoring at address 0
> > > thru byte (256/90)*(length *profile-array*)
> > > (si::display-prof) displays the results
> > > NIL
> > >
> > > b) run si::prof with the starting address you desire to
> > > examine, and a 'scale' parameter indicating how many counter
> > > profile array elements to allocate to each 256 bytes of code.
> > > You can see these addresses reported on loading binary
> > > modules, or you could use the DBEGIN value issued at
configure
> > > time. You could also try function-address. We need to make
> > > it easier to just say 'profile my whole program', but what I
> > > did was find the address of _init in gdb, find the value of
> > > heap_end in gdb, figure out a good scale for this amount of
> > > memory to correspond to a 1000000 byte array, and issue the
> > > following call for maxima:
> > >
> > > :lisp (si::prof 134522412 15)
> > >
> > > c) run some intesive code, I did load("tests.lisp");
> > >
> > > d) Turn off the profiler
> > >
> > > :lisp (si::prof 0 0)
> > >
> > > e) display the results, probably using the same scale and
> > > start address as in b):
> > >
> > > :lisp (si::display-profile 134522412 15)
> > >
> > > My output follows. There are a few gotchas in interpretation
> > > -- If a global function in GCL's core is separated from the
> > > next such function by a bunch of static functions, all counts
> > > for the static functions get lumped into the first's counter.
> > > The large values for 'enter_mark_origin' thus refers to the
> > > GBC time in the marker and sweeper located in between in the
> > > code. Also needs cleaning up.
> > >
> > > All user functions are not thus afflicted. But the core
> > > function counts are probably illustrative, as they may
indicate
> > > inefficiencies in the lisp compiler's optimization/inlining
of
> > > calls.
> > >
> > > I short, I'd appreciate seeing your version of the following:
> > >
> > > 0.10% ( 1): strerror
> > > 0.10% ( 1): memmove
> > > 0.39% ( 4): IapplyVector
> > > 0.39% ( 4): Iinvoke_c_function_from_value_stack
> > > 0.10% ( 1): make_fixnum1
> > > 0.10% ( 1): pack_hash
> > > 0.19% ( 2): intern
> > > 0.10% ( 1): Lintern
> > > 0.10% ( 1): Lunuse_package
> > > 0.10% ( 1): Lparse_namestring
> > > 0.10% ( 1): fLrationalp
> > > 0.10% ( 1): fLfunctionp
> > > 1.07% ( 11): eql
> > > 0.58% ( 6): equal
> > > 0.29% ( 3): init_predicate_function
> > > 0.10% ( 1): edit_double
> > > 0.78% ( 8): write_object
> > > 0.68% ( 7): Lwrite_char
> > > 0.10% ( 1): princ
> > > 0.19% ( 2): init_prog
> > > 0.58% ( 6): read_object
> > > 0.39% ( 4): NIL
> > > 0.19% ( 2): NIL
> > > 0.87% ( 9): Lread_char
> > > 0.10% ( 1): rl_putc_em
> > > 0.48% ( 5): symbol_function
> > > 0.10% ( 1): Lelt
> > > 1.55% ( 16): elt
> > > 0.39% ( 4): elt_set
> > > 0.87% ( 9): length
> > > 0.19% ( 2): nreverse
> > > 0.10% ( 1): fSclear_connection_state
> > > 0.19% ( 2): coerce_to_string
> > > 0.10% ( 1): get_string_start_end
> > > 0.19% ( 2): Lstring_neq
> > > 0.10% ( 1): Lmake_string
> > > 0.19% ( 2): Lstring_right_trim
> > > 0.10% ( 1): structure_ref
> > > 0.68% ( 7): symbol_value
> > > 1.84% ( 19): getf
> > > 0.10% ( 1): get
> > > 0.19% ( 2): remf
> > > 0.10% ( 1): remprop
> > > 0.19% ( 2): Lgetf
> > > 0.39% ( 4): check_type_symbol
> > > 0.10% ( 1): check_type_string
> > > 0.10% ( 1): check_type_cons
> > > 0.10% ( 1): Ltype_of
> > > 2.62% ( 27): alloc_object
> > > 3.30% ( 34): make_cons
> > > 0.39% ( 4): alloc_relblock
> > > 0.29% ( 3): fLrow_major_aref
> > > 0.10% ( 1): fSaset1
> > > 0.10% ( 1): fSget_aelttype
> > > 0.19% ( 2): gset
> > > 0.10% ( 1): array_allocself
> > > 0.10% ( 1): fLfill_pointer
> > > 0.48% ( 5): setq
> > > 0.10% ( 1): fLmakunbound
> > > 0.10% ( 1): fSset_gmp_allocate_relocatable
> > > 0.19% ( 2): new_bignum
> > > 0.10% ( 1): normalize_big_to_object
> > > 0.10% ( 1): mul_int_big
> > > 0.39% ( 4): normalize_big
> > > 0.10% ( 1): big_minus
> > > 0.19% ( 2): maybe_replace_big
> > > 0.39% ( 4): integer_quotient_remainder_1
> > > 0.19% ( 2): parse_key_new_new
> > > 0.19% ( 2): Lchar_eq
> > > 0.10% ( 1): Lchar_neq
> > > 0.10% ( 1): Lchar_upcase
> > > 0.10% ( 1): cplus
> > > 0.10% ( 1): init_error
> > > 1.94% ( 20): funcall
> > > 0.19% ( 2): funcall_no_event
> > > 0.10% ( 1): super_funcall
> > > 0.29% ( 3): super_funcall_no_event
> > > 0.10% ( 1): readc_stream
> > > 0.10% ( 1): unreadc_stream
> > > 0.58% ( 6): writec_stream
> > > 0.29% ( 3): flush_stream
> > > 0.39% ( 4): read_fasl_data
> > > 0.10% ( 1): Lformat
> > > 0.29% ( 3): fLformat
> > > 0.10% ( 1): frs_sch_catch
> > > 0.10% ( 1): call_or_link
> > > 0.48% ( 5): c_apply_n
> > > 3.39% ( 35): call_proc_new
> > > 31.62% ( 326): enter_mark_origin
> > > 0.10% ( 1): perm_writable
> > > 1.65% ( 17): car
> > > 1.65% ( 17): cdr
> > > 0.29% ( 3): kar
> > > 1.26% ( 13): list
> > > 0.19% ( 2): listA
> > > 0.10% ( 1): append
> > > 0.19% ( 2): copy_list
> > > 0.19% ( 2): Lcdr
> > > 0.10% ( 1): cddr
> > > 0.39% ( 4): Llast
> > > 0.39% ( 4): Lmake_list
> > > 0.10% ( 1): Lrevappend
> > > 0.29% ( 3): nconc
> > > 0.10% ( 1): Lreconc
> > > 0.10% ( 1): fixnum_add
> > > 0.19% ( 2): number_plus
> > > 0.19% ( 2): number_minus
> > > 0.19% ( 2): get_gcd
> > > 0.97% ( 10): number_compare
> > > 0.10% ( 1): Lall_the_same
> > > 0.10% ( 1): number_expt
> > > 0.10% ( 1): GET-INSTREAM
> > > 0.29% ( 3): READ-FROM-STRING
> > > 0.10% ( 1): TYPEP
> > > 0.10% ( 1): SYSTEM::NORMALIZE-TYPE
> > > 0.48% ( 5): SYSTEM::KNOWN-TYPE-P
> > > 0.29% ( 3): SUBTYPEP
> > > 0.10% ( 1): CONCATENATE
> > > 0.10% ( 1): SYSTEM::BAD-SEQ-LIMIT
> > > 0.10% ( 1): REMOVE
> > > 0.10% ( 1): DELETE
> > > 0.19% ( 2): POSITION
> > > 0.10% ( 1): SORT
> > > 0.10% ( 1): WITH-HASH-TABLE-ITERATOR
> > > 0.10% ( 1): user_match
> > > 0.10% ( 1): ASSQR
> > > 0.10% ( 1): SYS-FREE-MEMORY
> > > 0.19% ( 2): MGET
> > > 0.10% ( 1): MACLISP-TYPEP
> > > 0.19% ( 2): BOTHCASE-IMPLODE
> > > 0.10% ( 1): LIST-STRING
> > > 0.10% ( 1): TYO
> > > 0.39% ( 4): TYI
> > > 0.10% ( 1): FILE-TO-STRING
> > > 0.10% ( 1): ALPHALESSP
> > > 0.78% ( 8): MEMQ
> > > 0.10% ( 1): DELQ
> > > 0.29% ( 3): SAFE-GET
> > > 0.19% ( 2): GETL
> > > 0.10% ( 1): SUB
> > > 0.19% ( 2): ASSOL
> > > 0.10% ( 1): ASSOLIKE
> > > 0.10% ( 1): MAXIMA-SUBSTITUTE
> > > 0.19% ( 2): GETOP
> > > 0.19% ( 2): GETOPR
> > > 0.10% ( 1): $LISTP
> > > 0.10% ( 1): SPANG1
> > > 0.10% ( 1): $GETCHAR
> > > 0.10% ( 1): MEVALARGS
> > > 0.10% ( 1): SAFE-MGETL
> > > 1.36% ( 14): MEVAL1
> > > 0.10% ( 1): GETL-LM-FCN-PROP
> > > 0.10% ( 1): MGETL
> > > 0.10% ( 1): $SQRT
> > > 0.10% ( 1): $BINOMIAL
> > > 0.19% ( 2): ONEP1
> > > 0.39% ( 4): ZEROP1
> > > 0.19% ( 2): MNUMP
> > > 0.10% ( 1): RATNUMP
> > > 0.10% ( 1): MEXPTP
> > > 0.10% ( 1): $RATNUMP
> > > 0.10% ( 1): SPECREPCHECK
> > > 0.10% ( 1): CONSTANT
> > > 0.10% ( 1): MAXIMA-CONSTANTP
> > > 0.10% ( 1): MXORLISTP1
> > > 0.10% ( 1): CONSTFUN
> > > 0.10% ( 1): FREE
> > > 0.58% ( 6): SIMPLIFYA
> > > 0.29% ( 3): EQTEST
> > > 0.10% ( 1): RULECHK
> > > 0.10% ( 1): TIMESK
> > > 0.10% ( 1): PLS
> > > 0.10% ( 1): TESTT
> > > 0.10% ( 1): TESTTNEG
> > > 0.19% ( 2): SIMPTIMES
> > > 0.10% ( 1): STIMEX
> > > 0.10% ( 1): TMS
> > > 0.10% ( 1): SIGNUM1
> > > 0.19% ( 2): EXPTRL
> > > 0.10% ( 1): SIMPEXPT
> > > 0.29% ( 3): TIMESIN
> > > 0.58% ( 6): ALIKE1
> > > 0.10% ( 1): ALIKE
> > > 0.10% ( 1): ORDHACK
> > > 0.10% ( 1): RATNUMERATOR
> > > 0.39% ( 4): NTHKDR
> > > 0.10% ( 1): $MKEY
> > > 0.10% ( 1): MEVAL*
> > > 0.10% ( 1): KILL1
> > > 0.10% ( 1): REMALIAS
> > > 0.10% ( 1): STRING*
> > > 0.10% ( 1): $NOUNIFY
> > > 0.10% ( 1): PFLATTEN
> > > 0.10% ( 1): PMINUSP
> > > 0.10% ( 1): PQUOTIENT
> > > 0.19% ( 2): ALGORD
> > > 0.10% ( 1): PSIMP
> > > 0.10% ( 1): PCETIMES1
> > > 0.10% ( 1): PCTIMES
> > > 0.10% ( 1): PEXPTSQ
> > > 0.58% ( 6): $APROPOS
> > > 0.10% ( 1): DIVISORS
> > > 0.10% ( 1): COMPLETEVECTOR
> > > 0.10% ( 1): CFACTOR
> > > 0.19% ( 2): SAVEFACTORS
> > > 0.10% ( 1): FACTOROUT1
> > > 0.10% ( 1): PFACTOR1
> > > 0.10% ( 1): PSQUOREM1
> > > 0.10% ( 1): OLDCONTENT1
> > > 0.10% ( 1): PCONTENTZ
> > > 0.19% ( 2): $RATSIMP
> > > 0.10% ( 1): $FACTOR
> > > 0.10% ( 1): RATSETUP1
> > > 0.10% ( 1): GENSYM-READABLE
> > > 0.10% ( 1): ORDERPOINTER
> > > 0.10% ( 1): RATREP*
> > > 0.10% ( 1): RATF
> > > 0.29% ( 3): PREP1
> > > 0.10% ( 1): NEWVAR1
> > > 0.10% ( 1): PDISREP
> > > 0.10% ( 1): PDISREP!
> > > 0.10% ( 1): PDISREP2
> > > 0.10% ( 1): $RATDISREP
> > > 0.10% ( 1): CDISREP
> > > 0.10% ( 1): NEWVAR
> > > 0.10% ( 1): RADSORT
> > > 0.10% ( 1): RDIS*
> > > 0.10% ( 1): PRODCOEF
> > > 0.19% ( 2): FREEOF
> > > 0.10% ( 1): FLGREAT1
> > > 0.19% ( 2): STRING1
> > > 0.19% ( 2): MSIZE
> > > 0.10% ( 1): MSIZE-ATOM
> > > 0.10% ( 1): MSZ
> > > 0.10% ( 1): MSZ-MEXPT
> > > 0.29% ( 3): STRMDOIN
> > > 0.10% ( 1): NFORMAT
> > > 0.39% ( 4): FORM-MTIMES
> > > 0.10% ( 1): IMEMBER
> > > 0.10% ( 1): ALPHABETP
> > > 0.10% ( 1): ASCII-NUMBERP
> > > 0.10% ( 1): TYI-PARSE-INT
> > > 0.10% ( 1): ALIASLOOKUP
> > > 0.19% ( 2): GOBBLE-WHITESPACE
> > > 0.10% ( 1): PARSER-ASSOC
> > > 0.19% ( 2): READ-COMMAND-TOKEN-AUX
> > > 0.10% ( 1): READLIST
> > > 0.19% ( 2): SCAN-DIGITS
> > > 0.10% ( 1): COLLISION-CHECK
> > > 0.10% ( 1): MREAD
> > > 0.29% ( 3): ADD-LINEINFO
> > > 0.10% ( 1): TRIGINT
> > > 0.10% ( 1): $LISTOFVARS
> > > 0.19% ( 2): DIMENSION
> > > 0.10% ( 1): MAKESTRING
> > > 0.10% ( 1): DIMENSION-SUPERSCRIPT
> > > 0.10% ( 1): CHECKFIT
> > > 0.19% ( 2): CHECKBREAK
> > > 0.19% ( 2): OUTPUT
> > > 0.10% ( 1): DRAW-LINEAR
> > > 0.10% ( 1): D-SUMSIGN
> > > 0.48% ( 5): EXPLODEN
> > > 0.10% ( 1): CNTP
> > > 0.10% ( 1): LEARN
> > > 0.10% ( 1): LIKE
> > > 0.10% ( 1): DEQ
> > > 0.10% ( 1): TESTA*
> > > 0.10% ( 1): E1-
> > > 0.10% ( 1): PSTIMES
> > > 0.19% ( 2): PSEXPT1
> > > 0.10% ( 1): GET-ARRAY-POINTER
> > > 0.10% ( 1): SIMPLIM%INVERSE_JACOBI_DS
> > > 0.10% ( 1): %$ETEST
> > > Total ticks 1031
> > > 134522412
> > >
> > > f) I'd like suggestions on how to improve the usability here.
> > >
> > > 3) The gprof mode will require a bit more work, as recent
gprof in
> > > Linux calls monstartup authmatically in gcrt0.o, foiling
the
> > > existing strategy in the code.
> > >
> > > Take care,
> > >
> > >
> > >
> > > --
> > > Camm Maguire
address@hidden
> > >
==========================================================================
> > > "The earth is but one country, and mankind its citizens." --
Baha'u'llah
> > >
> > >
> > >
> > > _______________________________________________
> > > Gcl-devel mailing list
> > > address@hidden
> > > http://mail.gnu.org/mailman/listinfo/gcl-devel
> > >
> > >
> > >
> >
> > --
> > Camm Maguire
address@hidden
> >
==========================================================================
> > "The earth is but one country, and mankind its citizens." --
Baha'u'llah
> > ----------
> >
> >
> >
> >
> >
>
> --
> Camm Maguire address@hidden
>
==========================================================================
> "The earth is but one country, and mankind its citizens." --
Baha'u'llah
>
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah