BRR

Major Section:  BREAK-REWRITE

Example:
:brr t       ; enable
:brr nil     ; disable

General Form:
(brr flg)

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.