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, for example 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.

For ACL2 built on most host Common Lisps, you will see the string [RAW LISP] in the prompt at a break, to emphasize that one is inside a break and hence should quit from the break. For some host Common Lisps, the top-level prompt also contains the string [RAW LISP]. See prompt for how to control printing of that string.

The most reliable way to return to the ACL2 top level is by executing the following command: (abort!). Appropriate cleanup will then be done, which should leave you in an appropriate state.

However, you may be able to quit from the break in the normal Lisp manner (as with :q in GCL, :reset in Allegro CL, and q in CMU CL). If this attempt to quit is successful, it will return you to the innermost ACL2 read-eval-print loop, with appropriate cleanup performed first. 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.