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 books/misc/profiling.lisp.
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
Evaluation of (profile 'fn) redefines fn so that a count will be kept
of the calls of FN. The information recorded may be displayed, for example,
by invoking (memoize-summary) or (equivalently) (memsum).
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 :CONDITION and :INLINE
of memoize the value nil. Other keyword parameters for
memoize, which must not include :CONDITION, :CONDITION-FN, or
:INLINE, are passed through. To eliminate profiling, use
unmemoize; for example, to eliminate profiling for function fn,
evaluate (unmemoize 'fn).
You may find raw Lisp functions profile-all and 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.
