Profile-ACL2
profile essentially all ACL2 functions
Evaluating (profile-acl2) profiles each function symbol
admitted to ACL2 unless it is
- memoized,
- traced,
- in the package "COMMON-LISP", or
- otherwise illegal to memoize or profile (as per raw Lisp variables
*never-memoize-ht* and *profile-reject-ht*).
When profile-acl2 is invoked, it calls clear-memoize-statistics
to remove all profiling info displayed by memoize-summary.
Also see profile-all, which is similar but is not restricted to
functions defined in the ACL2 loop.
General form:
(profile-acl2 :start start ; default 0
:lots-of-info lots-of-info ; default t
:forget forget ; default nil
)
where all keywords are evaluated and optional, and:
- start (default: 0) is either an event name or a natural number,
to restrict to functions admitted after the given event or after the given
number of events, respectively;
- lots-of-info (default: t) determines whether the usual profiling
information is recorded (when lots-of-info is true) or not (when
lots-of-info is false); and
- forget (default: nil) is passed as the :forget argument for
each generated call of profile.
Note that profile-acl2 has an under-the-hood definition in raw Lisp,
and thus a trust tag (see defttag) is temporarily introduced while
loading its definition.
