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, :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.
