Major Section: MISCELLANEOUS
To enter the ACL2 command loop from Common Lisp, call the Common
lp (which stands for ``loop,'' as in ``read-eval-print
loop'' or ``command loop.'') The ACL2 command loop is actually
coded in ACL2 as the function
ld (which stands for ``load''). The
command loop is just what you get by loading from the standard
object input channel,
ld directly from
Common Lisp is possible but fragile because hard lisp errors or
aborts throw you out of
ld and back to the top-level of Common Lisp.
ld in such a way as to prevent this and is thus the
standard way to get into the ACL2 command loop. Also
see acl2-customization for information on the loading of an
All of the visible functionality of
lp is in fact provided by
which is written in ACL2 itself. Therefore, you should see ld
for detailed documentation of the ACL2 command loop. We sketch it
below, for novice users.
Every expression typed to the ACL2 top-level must be an ACL2 expression.
Any ACL2 expression may be submitted for evaluation. Well-formedness is checked.
Some well-formed expressions cannot be evaluated because they involve (at some level)
undefined constrained functions (see encapsulate). In addition, ACL2 does not
allow ``global variables'' in expressions to be evaluated. Thus,
(car '(a b c))
is legal and evaluates to
(car x) is not, because there is no
``global context'' or binding environment that gives meaning to the variable symbol
There is an exception to the global variable rule outlined above:
single-threaded objects (see stobj) may be used as global variables
in top-level expressions. The most commonly used such object is the
ACL2 ``current state,'' which is the value of the variable symbol
state. This variable may occur in the top-level form to be
evaluated, but must be passed only to ACL2 functions ``expecting''
as described in the documentation for
state and for
stobjs in general.
If the form returns a new state object as one of its
values, then that is considered the new ``current'' state for
the evaluation of the subsequent form. See state.
ACL2 provides some support for the functionality usually provided by global variables in a read-eval-print loop, namely the saving of the result of a computation for subsequent re-use in another expression. See assign and see @.
If the form read is a single keyword, e.g.,
special procedures are followed. See keyword-commands.
The command loop keeps track of the commands you have typed and allows you to review them, display them, and roll the logical state back to that created by any command. See history.
ACL2 makes the convention that if a top-level form returns three
values, the last of which is an ACL2 state, then the first is
treated as a flag that means ``an error occurred,'' the second is
the value to be printed if no error occurred, and the third is (of
course) the new state. When ``an error occurs'' no value is
printed. Thus, if you execute a top-level form that happens to
return three such values, only the second will be printed (and that
will only happen if the first is
nil!). See ld for details.