Q
Quit ACL2 (type :q) — reenter with (lp)
Example:
ACL2 !>:Q
The keyword command :q typed at the top-level of the ACL2 loop will
terminate the loop and return control to the Common Lisp top-level (or, more
precisely, to whatever program invoked lp). To reenter the ACL2 loop,
execute (acl2::lp) in Common Lisp. You will be in the same state as you
were when you exited with :q, unless during your stay in Common Lisp you
messed with the data structures representing the ACL2 state (including
files, property lists, and single-threaded objects).
You may also issue the command (value :q) to exit the ACL2 loop. More
generally, if the result of evaluating a form in the ACL2 loop is the error-triple (nil :q state), the ACL2 loop will be exited.
WARNING: The issuance of commands to raw Lisp may render your ACL2 session
unsound. Furthermore, evaluation of forms after exiting the ACL2 loop with
:q (or (value :q), etc.) is not guaranteed to agree with their
evaluation in the ACL2 loop. Specifically, Common Lisp may read an expression
with the backquote character (`) differently from how ACL2 reads the
expression. (The technical reason, in Common Lisp parlance, is that ACL2
installs its own readtable in the ACL2 loop, which includes a custom backquote
reader.) Results of evaluation may have surprising differences depending on
whether evaluation takes place in the ACL2 loop or in raw Lisp, as illustrated
by the following log produced using an ACL2 executable built on SBCL.
ACL2 !>(car (quote `(a b c)))
QUOTE
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
* (car (quote `(a b c)))
SB-INT:QUASIQUOTE
*
To minimize discrepancies (including that one) between ACL2 and raw Lisp,
use raw-mode instead of exiting the ACL2 loop.
Unlike all other keyword commands, typing :q is not equivalent to
invoking the function q. There is no function q.
