Major Section: OTHER
Examples: (LD "foo.lisp") ; read and evaluate each form in file ; "foo.lisp", in order (LD "foo.lisp" :ld-pre-eval-print t) ; as above, but print each form to standard ; character output just before it is evaluated
General Form: (LD standard-oi ; open obj in channel, stringp file name ; to open and close, or list of forms
; Optional keyword arguments: :dir ... ; use this add-include-book-dir directory :standard-co ... ; open char out or file to open and close :proofs-co ... ; open char out or file to open and close :current-package ... ; known package name :ld-skip-proofsp ... ; nil, 'include-book, or t ; (see ld-skip-proofsp) :ld-redefinition-action ... ; nil or '(:a . :b) :ld-prompt ... ; nil, t, or some prompt printer fn :ld-keyword-aliases ... ; an alist pairing keywords to parse info :ld-pre-eval-filter ... ; :all, :query, or some new name :ld-pre-eval-print ... ; nil, t, or :never :ld-post-eval-print ... ; nil, t, or :command-conventions :ld-evisc-tuple ... ; nil or '(alist nil nil level length) :ld-error-triples ... ; nil or t :ld-error-action ... ; :return!, :return, :continue or :error :ld-query-control-alist ... ; alist supplying default responses :ld-verbose ...) ; nil or t
Ld is the top-level ACL2 read-eval-print loop. (When you call
a little initialization is done in raw Common Lisp and then
Ld is also a general-purpose ACL2 file loader and a
Ld is actually a macro that expands to a
function call involving
Ld returns an ``error triple''
(mv erp val state) as explained below.
See rebuild for a variant of
ld that skips proofs.
The arguments to
ld, except for
:dir, all happen to be global
state. For example,
ld-verbose are global variables, which may be accessed via
(@ current-package) and
(@ ld-verbose). When
ld is called, it
``binds'' these variables. By ``binds'' we actually mean the variables are
globally set but restored to their old values on exit. Because
provides the illusion of state global variables being bound, they are
ld specials'' (after the Lisp convention of calling a variable
``special'' if it is referenced freely after having been bound).
Note that all arguments but the first are passed via keyword. Any variable
not explicitly given a value in a call retains its pre-call value, with the
ld-error-action, which defaults to
not explicitly specified.
Just as an example to drive the point home: If
"ACL2" and you typed
(ld *standard-oi* :current-package "MY-PKG")you would find yourself in (an inner) read-eval-print loop in which the current-package was
"MY-PKG". You could operate there as long as you wished, changing the current package at will. But when you typed
qyou would return to the outer read-eval-print loop where the current package would still be
ld repeatedly reads a form from
evaluates it, and prints its result to
standard-co. It does this until
the form is
q or evaluates to an error triple whose value
q, or until the input channel or list is emptied.
ld has many bells and whistles controlled by the
specials. Each such special is documented individually. For example, see
the documentation for
A more precise description of
ld is as follows. In the description below
we use the
ld specials as variables, e.g., we say ``a form is read from
standard-oi.'' By this usage we refer to the current value of the
named state global variable, e.g., we mean ``a form is read from the
current value of
standard-oi.'' This technicality has an important
implication: If while interacting with
ld you change the value of one of
ld specials, e.g.,
standard-oi, you will change the
ld, e.g., subsequent input will be taken from the new value.
ld specials are treated as channels:
standard-oi is treated
as an object input channel and is the source of forms evaluated by
proofs-co are treated as character output
channels and various flavors of output are printed to them. However, the
supplied values of these specials need not actually be channels; several
special cases are recognized.
If the supplied value of one of these is in fact an open channel of the
appropriate type, that channel is used and is not closed by
ld. If the
supplied value of one of these specials is a string, the string is treated as
a file name in (essentially) Unix syntax (see pathname) and a channel of the
appropriate type is opened to/from that file. Any channel opened by
during the binding of the
ld specials is automatically closed by
upon termination. If
proofs-co are equal
strings, only one channel to that file is opened and is used for both.
As a special convenience, when
standard-oi is a string and the
argument provided and not
nil, we look up
:dir in the table of
directories maintained by
add-include-book-dir, and prepend this
standard-oi to create the filename. (In this case,
however, we require that
standard-oi is a relative pathname, not an
absolute pathname.) For example, one can write
(ld "arithmetic/top-with-meta.lisp" :dir :system) to
particular system library. (Of course, you should almost always load books
include-book instead of
:dir is not specified, then a relative pathname is resolved
using the connected book directory; see cbd.
Several other alternatives are allowed for
standard-oi is a true list then it is taken as the list of forms to be
standard-oi is a list ending in an open channel, then
ld processes the forms in the list and then reads and processes the forms
from the channel. Analogously, if
standard-oi is a list ending a
string, an object channel from the named file is opened and
the forms in the list followed by the forms in the file. That channel is
closed upon termination of
ld specials are handled more simply and generally have to
be bound to one of a finite number of tokens described in the
entries for each
ld special. Should any
ld special be supplied an
inappropriate value, an error message is printed.
ld prints the message ``ACL2 loading
name names the file or channel from which forms are being
read. At the conclusion of
ld, it will print ``Finished loading name''
ld repeatedly executes the ACL2 read-eval-print step, which may
be described as follows. A prompt is printed to
ld-prompt is non-
nil. The format of the prompt is determined
ld-prompt. If it is
t, the default ACL2 prompt is used.
If it is any other non-
nil value then it is treated as an ACL2 function
that will print the desired prompt. See ld-prompt. In the exceptional
ld's input is coming from the terminal
its output is going to a different sink (i.e.,
standard-co is not
*standard-co*), we also print the prompt to the terminal.
Ld then reads a form from
standard-oi. If the object read is a
ld constructs a ``keyword command form'' by possibly reading
several more objects. See keyword-commands. This construction process is
sensitive to the value of
ld-keyword-aliases. See ld-keyword-aliases.
Otherwise, the object read is treated as the command form.
Ld next decides whether to evaluate or skip this form, depending on
ld-pre-eval-filter. Initially, the filter must be either
:query, or a new name. If it is
:all, it means all forms are
evaluated. If it is
:query, it means each form that is read is displayed
and the user is queried. Otherwise, the filter is a name and each form that
is read is evaluated as long as the name remains new, but if the name is ever
introduced then no more forms are read and
If the form is to be evaluated, then
ld first prints the form to
t. With this feature,
ld can process an input file or form list and construct a script of the
session that appears as though each form was typed in.
Ld then evaluates the form, with
state bound to the current
state. The result is some list of (multiple) values. If a state
is among the values, then
ld uses that state as the subsequent
ld may interpret the result as an
``error.'' See ld-error-triples. We first discuss
ld's behavior if no
error signal is detected (either because none was sent or because
ignoring them because
ld-error-triples is nil).
In the case of a non-erroneous result,
ld does two things: First, if the
logical world in the now current state is different than the
world before execution of the form,
ld adds to the world a
``command landmark'' containing the form evaluated.
See command-descriptor. Second,
ld prints the result to
standard-co, but only if
ld-post-eval-print is not
result is printed as a list of (multiple) values unless
ld-error-triples is t, and the result is an ``error triple'', i.e., of
(mv * * state). In that case, only the non-erroneous ``value''
component of the result is printed. See ld-post-eval-print.
ld prints anything (whether the input form, a query, or
some results) it ``eviscerates'' it if
ld-evisc-tuple is non-
Essentially, evisceration is a generalization of Common Lisp's use
*print-length* to hide large substructures.
See evisc-tuple and also see set-iprint.
We now return to the case of a form whose evaluation signals an error. In
ld first restores the ACL2 logical world to what it was
just before the erroneous form was evaluated. Thus, a form that partially
changes the world (i.e., begins to store properties) and then signals an
error, has no effect on the world. You may see this happen on
commands that execute several events (e.g., an
progn of several
defuns): even though the output makes it
appear that the initial events were executed, if an error is signalled
by a later event the entire block of events is discarded.
After rolling back,
ld takes an action determined by
ld-error-action. If the action is
iterates the read-eval-print step. Note that nothing suggestive of the value
of the ``erroneous'' form is printed. If the action is
terminates normally; similarly if the action is
:return!, but a special
value is returned that can cause superior
ld commands to terminate;
see ld-error-action for details. If the action is
terminates signalling an error to its caller. If its caller is in fact
another instance of
ld and that instance is watching out for error
signals, the entire world created by the inner
ld will be discarded
by the outer
ld if the inner
ld terminates with an error.
Ld returns an error triple,
(mv erp val state).
nil indicating whether an error is being signalled. If no error is
val is the ``reason''
ld terminated and is one of
q was read),
:eof (meaning the input source
:error (meaning an error occurred but has been supressed),
:filter (meaning the
ld), or a
cons pair whose first component is the symbol
:STOP-LD, which typically
indicates that an error occurred while the value of variable
:RETURN!. See ld-error-action for
details of this last case.