Dmr
Dynamically monitor rewrites and other prover activity
In addition to utilities that allow you to set breakpoints or print
rewriting information to the screen — see break-rewrite (also see
related utility with-brr-data) — 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 updates a file (the ``dmr file'') containing the relevant
information, and an Emacs component that frequently updates an Emacs
buffer (the ``dmr buffer'') with the contents of that file. 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 to the terminal. 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-acl2.el from a suitable directory; see emacs. Otherwise, load into Emacs the file monitor.el from that same
directory. (You only need to do that once in your Emacs session.) 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 let us consider line 13 and the two lines below it. The phrase
"'Applying (:REWRITE MOD-ZERO . 2)" says that the indicated rewrite
rule is being considered for application to the current term. There are very
weak criteria for ``Applying'' to be printed: the rule must be enabled, and
top-level function symbols much suitably match for the term and the rule. In
particular, the ``Applying'' line does not imply that the rule actually
matches the term. That said: in the case of line 13, matching clearly was
successful, since line 14 indicates an attempt to establish the rule's fourth
hypothesis.
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 the
indentation 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) will automatically enable the
debugger if it is not already enabled and not fully disabled with value
:never (see set-debugger-enable). If such automatic enabling
takes place, then (dmr-stop) will restore the old setting of the debugger
unless, after (dmr-start) enables the debugger but before (dmr-stop)
is called, you call set-debugger-enable (or more precisely: function
set-debugger-enable-fn is called).
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.
