Common Lisp breaks
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 ``
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
The most reliable way to return to the ACL2 top level is by executing the
However, you may be able to quit from the break in the normal Lisp manner