Major Section: ACL2-BUILT-INS
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 or CCL, :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.
