BREAKS

Major Section:  MISCELLANEOUS

Example:
Broken at PROVE.  Type :H for Help.
>>:Q


ACL2 !>

If a break occurs, e.g. because of a bug in ACL2 or a user interrupt, the break will run a Common Lisp read-eval-print loop, not an ACL2 read-eval-print loop. This may not be obvious if the prompts in the two loops are similar. Because you are typing to a Common Lisp evaluator, you must be careful. It is possible to damage your ACL2 state in irreparable ways by executing non-ACL2 Common Lisp. It is even possible to disrupt and render inaccurate the interrupted evaluation of a simple ACL2 expression.

Quitting from the break (as with :q in GCL, :reset in Allegro CL, and q in CMU CL) will return to the innermost ACL2 read-eval-print loop. Before the loop is continued, any pending cleanup forms from acl2-unwind-protects are evaluated (unless acl2::*acl2-panic-exit-flg* is non-nil, in which case no cleanup is done).

If you submit the token #. to raw lisp break, an abort is generally executed. (Some underlying Lisp systems, however, reset the read table (*readtable*), in which case you should type a number after #. and then follow the directions in the preceding paragraph.) Control is passed to the outermost ACL2 read-eval-print loop (lp). Again, unwind-protection cleanup forms are executed first.