The Common Lisp entry to ACL2
To enter the ACL2 command loop from Common Lisp, call the
Common Lisp program
All of the visible functionality of
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,
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''
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.,
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