DMR

dynamically monitor rewrites and other prover activity 
Major Section:  OTHER

In addition to utilities that allow you to set breakpoints or print rewriting information to the screen -- see break-rewrite -- ACL2 provides a utility for watching the activity of the rewriter and some other proof processes, in real time. This utility is called ``dmr'', which is an acronym for ``dynamically monitor rewrites''. The utility comes in two parts: an ACL2 component that frequently writes a file (the ``dmr file'') containing the relevant information, and an Emacs component that frequently displays the contents of that file in an Emacs buffer (the ``dmr buffer''). Other editors could, in principle, be programmed to display that file; anyone developing such a capability is invited to contribute it to the ACL2 community.

The dmr utility can be extremely helpful for expensive proofs, especially when ACL2 is not providing any output. The break-rewrite and accumulated-persistence utilities may be a bit easier to use, so you might want to try those first. But the dmr utility can be a very helpful debugging aide, as it can visually give you a sense of where ACL2 is spending its time.

The Emacs portion of this utility is already loaded if you load the distributed Emacs file emacs/emacs-acl2.el. Otherwise, invoke the following Emacs command, say by typing Control-X Control-E after the right parenthesis, where DIR is the directory of your ACL2 distribution. 

(load "<DIR>/emacs/monitor.el") ; absolute pathnames might work best
You only need to do that once. Then each time you want to observe the rewriter in action, invoke the following to see it displayed in a buffer, which we call the ``dmr buffer'': 
Control-t 1
But first you will need to enable monitoring at the ACL2 level: 
(dmr-start)
Monitoring has some cost. So if you have started it, then at some point you may want to turn it off when not using it. Any time the dmr buffer (generally called "acl2-dmr-<user_name>") is not visible, Emacs monitoring is turned off. You can also turn off Emacs monitoring explicitly, with: 
Control-t 2
At the ACL2 level you can disable monitoring as follows: 
(dmr-stop)

Interpreting the dmr buffer display.

We explain the dmr buffer display by way of the following example. It is a snapshot of a dmr buffer taken from one of the community books, books/workshops/2004/legato/support/proof-by-generalization-mult.lisp. 

 0. (DEFTHM . WP-ZCOEF-G-MULTIPLIES)
 1. SIMPLIFY-CLAUSE
   2. Rewriting (to simplify) the atom of literal 18; argument(s) 1
   4. Rewriting (to simplify) the expansion; argument(s) 3|2
   7. Applying (:DEFINITION WP-ZCOEF-G)
*  8. Rewriting (to simplify) the rewritten body; argument(s) 2|1|2|2
*  13. Applying (:REWRITE MOD-ZERO . 2)
*    14. Rewriting (to establish) the atom of hypothesis 4
*    15. Applying (:META META-INTEGERP-CORRECT)
Each line indicates an ACL2 activity that leads to the activity shown on the line just below it. Moreover, lines are sometimes collapsed to make the display more compact. Consider for example the first few lines. Above, we are proving a theorem named WP-ZCOEF-G-MULTIPLIES. Lines 1 and 2 show the clause simplification process invokes the rewriter on the 18th literal. (Recall that a clause is a disjunction of literals; for example the clause {(NOT A), (NOT B), C} would be displayed as (IMPLIES (AND A B) C).) This 18th literal mentioned on line 2 is a function call (f arg1 ...), and ``argument(s) 1'' indicates that the rewriter, which works inside-out, is considering the first argument (``arg1''). Thus the display could instead have shown the following. 
   2. Rewriting (to simplify) the atom of literal 18
   3. Rewriting (to simplify) the first argument
   4. Rewriting (to simplify) the expansion; argument(s) 3|2
But it saved space to combine lines 2 and 3. Line 4 suggests that the above arg1 is a function call that has been opened up because of an :expand hint or, perhaps, an expansion directed explicitly by the prover (as can happen during induction). The annotation ``argument(s) 3|2'' then indicates that the rewriter is diving into the third argument of the expansion, and then into the second argument of that. Let us call the result term7 (since it is the one to be considered on line 7).

Now consider the next two lines: 

   7. Applying (:DEFINITION WP-ZCOEF-G)
*  8. Rewriting (to simplify) the rewritten body; argument(s) 2|1|2|2
Line 7 is saying that term7 (defined above) is modified by applying the definition of WP-ZCOEF-G to it. Line 8 then says that the body of this definition has been rewritten (with its formals bound to the actuals from term7) and the rewriter is diving into the subterms of that rewritten body, as indicated. Notice also that line 8 is the first line marked with an asterisk (``*'') in the margin. This line is the first that is different from what was shown the previous time the display was updated (about 1/10 second earlier, by default). When a line is marked with an asterisk, so are all the lines below it; so the lines without an asterisk are those that have been stable since the last display. In this example we may see line 7 marked without an asterisk for a while, which suggests that the rule (:DEFINITION WP-ZCOEF-G) is expensive. (Also see accumulated-persistence.) In general, a line that persists for awhile without a leading asterisk can suggest why the proof is taking a long time.

Finally, note the indentation of line 14 relative to line 13. Extra indentation occurs when an attempt is being made to relieve a hypothesis (i.e., rewrite it to t). In particular, rewrites that will be incorporated directly into a (top-level) literal are all indented just two spaces, starting with the first rewrite directly under a process such as SIMPLIFY-CLAUSE (shown line 1 above). If the indentation is at least the value of raw Lisp variable *dmr-indent-max* (by default, 20), then indenttion is restricted to that column, but ACL2 prints {n} where n is the column that would have been used for indentation if there were no maximum.

You can move the cursor around in the dmr buffer even while it is being updated. But emacs will attempt to keep the cursor no later than the first asterisk (``*'') in the margin. Thus, you can move the cursor around in the stable part of the display, and emacs will keep the cursor in that stable part.

WARNING: Things could go terribly wrong if the same user runs two different ACL2 sessions with dmr active, because the same file will be written by two different ACL2 processes.

WARNING: For dmr to work, emacs and ACL2 need to be run on the same machine because the file used to communicate between ACL2 and emacs is under /tmp. Except, you can probably hack around that restriction by changing *dmr-file-name* in ACL2 (in raw Lisp) and correspondingly in Emacs file monitor.el.

More generally, advanced users are welcome to search for the string 

User-settable dmr variables
in ACL2 files interface-raw.lisp and emacs/monitor.el in order to customize their dmr environments.

In order to update the dmr file with the latest stack information, interrupt ACL2 and then evaluate: (dmr-flush). In order to support resumption of the interrupted proof (assuming your host Common Lisp supports resumption), evaluation of (dmr-start) automatically causes evaluation of the form (set-debugger-enable t); see set-debugger-enable.

Note for users of the experimental extension ACL2(p) (see parallelism): when waterfall-parallelism has been set to a non-nil value (see set-waterfall-parallelism), statistics about parallel execution are printed instead of the usual information.