Brr
To enable or disable the breaking of rewrite rules
Example:
:brr t ; enable
(brr t) ; enable (same as above)
(brr t t) ; enable with less output (rarely invoked interactively)
:brr nil ; disable
General Form:
(brr flg &optional quietp)
where flg and the optional quietp argument evaluate 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.''
For a more thorough introduction to the break rewrite system see break-rewrite. For a related proof debugging utility see with-brr-data.
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. 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, Console Interrupts, and Subsidiary Prover Calls: If the system is
operating in brr mode and you break into raw Lisp (as by causing a
console interrupt or happening upon a signaled Lisp error; see breaks),
you can return to the ACL2 top-level, outside any break-rewrite environment,
by executing (abort!). Otherwise, the normal way to quit
from such a raw Lisp 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 interrupt or error break happens to occur while ACL2 is
within a break-rewrite break (in which it is preparing to read brr-commands), the abort will merely return to break-rewrite break. Upon
exiting that environment, normal theorem proving is continued (and the
break-rewrite breaks may be entered again in response to subsequent monitored
rule applications). In addition, if while in a break-rewrite break, say at
depth d, you invoke the theorem prover recursively as by typing a thm or defthm or defun command to break-rewrite, recursive
breaks may occur with depths starting at d+1. This can get confusing
because it may appear that the ongoing (sub-)proofs are part of the original
proof when in fact the system is just carrying out your commands.
Subtopics
- Brr-evisc-tuple
- Determines partial suppression of output from brr-commands
- Set-brr-evisc-tuple
- Set the brr-evisc-tuple
