Major Section: BREAK-REWRITE
Example: :brr t ; enable :brr nil ; disable General Form: (brr flg)where
flg evaluates to t or nil. This function modifies
state so that the attempted application of certain rewrite rules are
``broken.'' ``Brr'' stands for ``break-rewrite'' and can be thought of as
a mode with two settings. The normal mode is ``disabled.''When brr mode is ``enabled'' the ACL2 rewriter monitors the attempts to
apply certain rules and advises the user of those attempts by entering an
interactive wormhole break. From within this break the user can watch
selected application attempts. See break-rewrite. The user can also
interact with the system during brr breaks via brr-commands.
The rules monitored are selected by using the monitor and
unmonitor commands. It is possible to break a rune ``conditionally''
in the sense that an interactive break will occur only if a specified
predicate is true of the environment at the time of the attempted
application. See monitor and see unmonitor.
Even if a non-empty set of rules has been selected, no breaks will occur
unless brr mode is enabled. Thus, the first time in a session that you
wish to monitor a rewrite rule, use :brr t to enable brr mode.
Thereafter you may select runes to be monitored with monitor and
unmonitor with the effect that whenever monitored rules are tried (and
their break conditions are met) an interactive break will occur. Be advised
that when brr mode is enabled the rewriter is somewhat slower than
normal. Furthermore, that sluggishness persists even if no runes are
monitored. You may regain normal performance -- regardless of what runes
are monitored -- by disabling brr mode with :brr nil.
Why isn't brr mode disabled automatically when no runes are monitored?
More generally, why does ACL2 have brr mode at all? Why not just test
whether there are monitored runes? If you care about the answers,
see why-brr.
BRR Mode and Console Interrupts: If the system is operating in brr mode
and you break into raw Lisp (as by causing a console interrupt or happening
upon a signalled Lisp error; see breaks), you can return to the ACL2
top-level, outside any brr environment, by executing
(abort!). Otherwise, the normal way to quit from such a break
(for example :q in GCL, :reset in Allegro CL, and q in CMU CL)
will return to the innermost ACL2 read-eval-print loop, which may or may not
be the top-level of your ACL2 session! In particular, if the break happens
to occur while ACL2 is within the brr environment (in which it is
preparing to read brr-commands), the abort will merely return to that
brr environment. Upon exiting that environment, normal theorem proving
is continued (and the brr environment may be entered again in response to
subsequent monitored rule applications). Before returning to the brr
environment, ACL2 ``cleans up'' from the interrupted brr processing.
However, it is not possible (given the current implementation) to clean up
perfectly. This may have two side-effects. First, the system may
occasionally print the self-explanatory ``Cryptic BRR Message 1'' (or 2),
informing you that the system has attempted to recover from an aborted
brr environment. Second, it is possible that subsequent brr behavior
in that proof will be erroneous because the cleanup was done incorrectly.
The moral is that you should not trust what you learn from brr if you
have interrupted and aborted brr processing during the proof. These
issues do not affect the behavior or soundness of the theorem prover.
