Profile-all
profile essentially all functions
Evaluating (profile-all) profiles each function symbol
in a package known 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-all is invoked, it calls clear-memoize-statistics
to remove all profiling info displayed by memoize-summary.
Also see profile-ACL2, which is similar but is restricted to
functions defined in the ACL2 loop.
General form:
(profile-all :lots-of-info lots-of-info ; default t
:forget forget ; default nil
:pkg pkg ; default nil
)
where all keywords are evaluated and optional, and:
- 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).
- forget (default: nil) is passed as the :forget argument for
each generated call of profile; and
- pkg, when supplied, is a package name or list of package names to use
in place of the default, which is the list of names of all packages known to
ACL2 except for packages "ACL2-INPUT-CHANNEL",
"ACL2-OUTPUT-CHANNEL", "COMMON-LISP", and "KEYWORD".
Note that profile-all has an under-the-hood definition in raw Lisp,
and thus a trust tag (see defttag) is temporarily introduced while
loading its definition.
