PROFILE

turn on profiling for one function
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 distributed 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.