BREAKS

Major Section:  MISCELLANEOUS

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


ACL2 !>

You may interrupt the system by typing various control character sequences. The precise sequences are determined by the host Lisp and operating system environment. For example, in GCL and Allegro Common Lisp, a console interrupt is caused by typing ``ctrl-c''. If, however, the GCL or Allegro is running in an Emacs shell buffer, one must type ``ctrl-c ctrl-c''.

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). Note that if you are within a brr environment when the break occurs, quitting from the break will only return you to that environment, not to the top of ACL2's read-eval-print loop.

If you submit the token #. to the 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.