Major Section: EVENTS
NOTE: An alternative to this utility, which has a lot less functionality but
doesn't depend on the experimental extension of ACL2 mentioned just below,
may be found in community book
This documentation topic relates to an experimental extension of ACL2 under
development by Bob Boyer and Warren Hunt. See hons-and-memoization for a
general discussion of memoization, on which this
profile utility is
built, and the related features of hash consing and applicative hash tables.
Profile can be useful in Common Lisp debugging and performance analysis,
including examining the behavior of ACL2 functions.
Example: (profile 'fn) ; keep count of the calls of fn (profile 'fn ; as above, with with some memoize options :trace t :forget t) (memsum) ; report statistics on calls of memoized functions (e.g., fn) (clear-memoize-statistics) ; clear memoization (and profiling) statistics
(profile 'fn) redefines
fn so that a count will be kept
of the calls of FN. The information recorded may be displayed, for example,
) or (equivalently)
If you wish to gather fresh statistics for the evaluation of a top-level
form, see clear-memoize-statistics.
Profile is just a macro that calls
memoize to do its work.
Profile gives the two keyword parameters
memoize the value
nil. Other keyword parameters
memoize, which must not include
:recursive, are passed through. To eliminate profiling, use
unmemoize; for example, to eliminate profiling for function
You may find raw Lisp functions
profile-acl2 to be
useful. Please contact the ACL2 developers if you want versions of these
functions to be executable from inside the ACL2 read-eval-print loop.