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 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. Such ``clean up'' may also occur when you call the prover from within
the brr environment (for example using defthm or thm, or
even defun or any other event that invoke the prover), unless
you invoke :brr nil before making that call. These issues do not affect
the behavior or soundness of the theorem prover.
Subtopics
- Brr-evisc-tuple
- Determines partial suppression of output from brr-commands
- Show-brr-evisc-tuple
- Display the brr-evisc-tuple
- Set-brr-evisc-tuple
- Set the brr-evisc-tuple
