Profile
Turn on profiling for one function
NOTE: An alternative to this utility, which has significantly less
functionality but doesn't use hons-enabled features of ACL2, may be
found in community book books/misc/profiling.lisp. 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 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
:recursive of memoize the value nil. Other keyword
parameters for memoize, which must not include :condition,
:condition-fn, or :recursive, are passed through. To eliminate
profiling, use unmemoize; for example, to eliminate profiling for
function fn, evaluate (unmemoize 'fn).
Functions profile-all and profile-ACL2 are available for
profiling all functions or all ACL2 functions, respectively.
Subtopics
- Profile-all
- profile essentially all functions
- Profile-ACL2
- profile essentially all ACL2 functions
