|
|
|---|
|
|
|
|---|
Initiate the printing of profiling information to view in Emacs
The following example from Bob Boyer shows how to use this feature.
acl2 (include-book "centaur/memoize/old/watch" :dir :system :ttags :all) :q (watch)
The output at the terminal will show a file name such as
(lp) (defun foo (x) (declare (xargs :guard t)) x) (memoize 'foo) (foo 1) (foo 1) (foo 2)
You can look at the above ``temporary'' file and see some interesting information related to features provided by your (hons-enabled) ACL2 executable. For a further experiment, continue in ACL2 as follows.
:q (profile-acl2) ; could take a minute or more (lp) :mini-proveall
The buffer for the above file will now provide reports on the 20 functions
that used the most time during the
The documentation below was directly derived from a Lisp documentation
string formerly in
WATCH is a raw Lisp function that initiates the printing of profiling information. (WATCH) sets *WATCH-FILE* to the string that results from the evaluation of *WATCH-FILE-FORM*, a string that is to be the name of a file we call the 'watch file'. In Clozure Common Lisp, (WATCH) also initiates the periodic evaluation of (WATCH-DUMP), which evaluates the members of the list *WATCH-FORMS*, but diverts characters for *STANDARD-OUTPUT* to the watch file. The value of *WATCH-FILE* is returned by both (WATCH) and (WATCH-DUMP). (WATCH-KILL) ends the periodic printing to the watch file. You are most welcome to, even encouraged to, change the members of *WATCH-FORMS* to have your desired output written to the watch file. Often (MEMOIZE-SUMMARY) is a member of *WATCH-FORMS*. It prints information about calls of memoized and/or profiled functions. Often (PRINT-CALL-STACK) is a member of *WATCH-FORMS*. It shows the names of memoized and/or profiled functions that are currently in execution and how long they have been executing. We suggest the following approach for getting profiling information about calls to Common Lisp functions: 0. Invoke (WATCH). 1. Profile some functions that have been defined. For example, call (PROFILE-FN 'foo1), ... Or, for example, call PROFILE-FILE on the name of a file that contains the definitions of some functions that have been defined. Or, as a perhaps extreme example, invoke (PROFILE-ACL2), which will profile many of the functions that have been introduced to ACL2, but may take a minute or two. Or, as a very extreme example, invoke (PROFILE-ALL), which will profile many functions, but may take a minute or two. 2. Run a Lisp computation of interest to you that causes some of the functions you have profiled to be executed. 3. Invoke (WATCH-DUMP). 4. Examine, perhaps in Emacs, the watch file, whose name was returned by (WATCH-DUMP). The watch file contains information about the behavior of the functions you had profiled or memoized during the computation of interest. From within ACL2, you may MEMOIZE any of your ACL2 Common Lisp compliant ACL2 functions. One might MEMOIZE a function that is called repeatedly on the exact same arguments. Deciding which functions to memoize is tricky. The information from (WATCH-DUMP) helps. Sometimes, we are even led to radically recode some of our functions so that they will behave better when memoized. In Emacs, the command 'M-X AUTO-REVERT-MODE' toggles auto-revert mode, i.e., causes a buffer to exit auto-revert mode if it is in auto-revert mode, or to enter auto-revert mode if it is not. In other words, to stop a buffer from being auto-reverted, simply toggle auto-revert mode; toggle it again later if you want more updating. 'M-X AUTO-REVERT-MODE' may be thought of as a way of telling Emacs, 'keep the watch buffer still'. In Clozure Common Lisp, if the FORCE-DOG argument to WATCH (default NIL) is non-NIL or if (LIVE-TERMINAL-P) is non-NIL a 'watch dog' thread is created to periodically call (WATCH-DUMP). The thread is the value of *WATCH-DOG-PROCESS*. See documentation strings in file books/centaur/memoize/old/watch-raw.lsp for further details.