Ld
The ACL2 read-eval-print loop, file loader, and command processor
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 ... ; directory spec if standard-oi is a string
: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
:useless-runes ... ; :write/:read/:read?/n/-n/nil
; (-100 < n < 0 or 0 < n <= 100)
; (see useless-runes)
: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-missing-input-ok ... ; nil, t, :warn, or warning message
: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, :error,
; or (:exit N)
:ld-query-control-alist ... ; alist supplying default responses
:ld-verbose ...) ; nil or t
:ld-always-skip-top-level-locals ; nil or t
:ld-user-stobjs-modified-warning ...) ; nil, t, or :same
Ld is the top-level ACL2 read-eval-print loop. (When you call lp, a little initialization is done in raw Common Lisp and then ld is
called.) Ld is also a general-purpose ACL2 file loader and a command interpreter. Ld is actually a macro that expands to a function
call involving state. Ld returns an ``error triple'' (mv erp
val state) as explained below. (For much more on error triples, see programming-with-state.)
See rebuild for a variant of ld that skips proofs. See output-to-file for examples showing how to redirect output to a file.
The arguments to ld, except for :dir, all happen to be global
variables in state (see state and see programming-with-state). For example, 'current-package and
'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 ld
provides the illusion of state global variables being bound, they are
generally called ``ld specials'' (after the Lisp convention of calling a
variable ``special'' if it is referenced freely after having been bound). (We
say ``generally'' because technically, current-package and
useless-runes are not considered to be ld specials.)
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
exception of :ld-error-action, which generally defaults to
:return! if not explicitly specified.
Just as an example to drive the point home: If current-package is
"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
:q you would return to the outer read-eval-print loop where the
current package would still be "ACL2".
Roughly speaking, ld repeatedly reads a form from standard-oi,
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
component is :q, or until the input channel or list is emptied.
However, ld has many bells and whistles controlled by the ld
specials. Each such special is documented individually. For example, see the
documentation for standard-oi, current-package, useless-runes, ld-pre-eval-print, etc.
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 the ld specials, e.g., 'standard-oi, you will
change the behavior of ld, e.g., subsequent input will be taken from the
new value.
Three ld specials are treated as channels: standard-oi is
treated as an object input channel and is the source of forms evaluated by
ld; standard-co and 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
ld during the binding of the ld specials is automatically closed by
ld upon termination. If standard-co and proofs-co are
strings that represent the same file, 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
:dir argument is provided and not nil, we look up :dir just as
is done for include-book; also see add-include-book-dir,
add-include-book-dir!, and project-dir-alist. Thus a suitable
directory is prepended to create the filename. Note that standard-oi
must be a string that is a relative pathname, not an absolute pathname. For
example, one can write (ld "arithmetic/top-with-meta.lisp" :dir
:system) to ld that particular community-books library. (Of
course, for certified books you should almost always use include-book instead of ld.) If :dir is not specified, then a
relative pathname is resolved using the connected book directory; see cbd. If you want to load a list of forms, then consider prepending a call of
set-cbd to that list rather than using :dir, which is not
supported when standard-oi is a list.
Several other alternatives are allowed for standard-oi. If standard-oi is a true list then it is taken as the list of forms to be
processed. If 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 input channel from the named file is opened and ld
processes the forms in the list followed by the forms in the file. That
channel is closed upon termination of ld.
In the cases that a string is to be converted to an object input channel
— that is, when standard-oi is a string or is a list ending in a
string — an error occurs by default if the conversion fails, presumably
because the file named by the string does not exist. However, if keyword
argument :ld-missing-input-ok is t, then ld immediately returns
without error in this case, but without reading or executing any forms, as
though standard-oi is nil and keyword arguments :ld-verbose and
:ld-prompt both have value nil. The other legal values for
:ld-missing-input-ok are nil, which gives the default behavior, and
:warn, which behaves the same as t except that a warning is printed,
which contains the same information as would be printed for the default error
described above.
The remaining ld specials are handled more simply and generally have
to be bound to one of a finite number of tokens described in the :doc entries for each ld special. Should any ld special be supplied
an inappropriate value, an error message is printed.
Next, if ld-verbose is t, ld prints the message ``ACL2
loading name'' where name names the file or channel from which forms are
being read. At the conclusion of ld, it will print ``Finished loading
name'' if ld-verbose is t.
One may generally omit ld-user-stobjs-modified-warning except when
calling ld in the body of a definition. In that case this keyword
argument is required, and the value t is recommended. With that value, a
warning will generally be printed if a user-defined stobj is modified
by the call of ld; value nil avoids such warnings, and value
:same causes the value to be inherited from the existing value (generally
from a superior call of ld). A discussion of these warnings is highly
recommended reading before you give a value other than t; see user-stobjs-modified-warnings.
Finally, ld repeatedly executes the ACL2 read-eval-print step, which
may be described as follows. A prompt is printed to standard-co if ld-prompt is non-nil. The format of the prompt is determined by 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 case where ld's input is coming
from the terminal (*standard-oi*) but 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 keyword, 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.
(Technical Aside. Some special handling takes place when ld is called
in the scope of local, as in (local (ld <C>)) for a command,
<C>. In that case, after <C> is evaluated, then if the result is an
error-triple and <C> is not already of the form (local <C0>),
then when the command is stored in the ACL2 world it is stored as
(local <C>) instead of <C>. See ld-history for a similar
treatment of local commands. End of Technical Aside.)
Ld next decides whether to evaluate or skip this form, depending on
ld-pre-eval-filter. Initially, the filter must be either :all,
: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 ld terminates. See ld-pre-eval-filter.
If the form is to be evaluated, then ld first prints the form to
standard-co, if ld-pre-eval-print is 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. See ld-pre-eval-print.
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 current state.
Depending on ld-error-triples, 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 ld is 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 nil. The
result is printed as a list of (multiple) values unless ld-post-eval-print is :command-conventions, ld-error-triples is
t, and the result is an error-triple, i.e., of the form (mv * *
state). In that case, only the non-erroneous ``value'' component of the
result is printed. See ld-post-eval-print.
Whenever ld prints anything (whether the input form, a query, or some
results) it ``eviscerates'' it if ld-evisc-tuple is non-nil.
Essentially, evisceration is a generalization of Common Lisp's use of
*print-level* and *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
this case, 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 encapsulate or
a progn of several defuns): even though the output makes it
appear that the initial events were executed, if an error is signaled
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 :continue, ld merely iterates
the read-eval-print step. Note that nothing suggestive of the value of the
``erroneous'' form is printed. If the action is :return, ld
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 :error, ld
terminates signaling 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. Note that if the action is (:exit N), then there is no rolling
back, because ACL2 quits immediately with exit status N.
Ld returns an error triple, (mv erp val state). Erp is
t or nil indicating whether an error is being signaled. If no error
is signaled, val is the ``reason'' ld terminated and is one of
:exit (meaning :q was read), :eof (meaning the input
source was exhausted), :error (meaning an error occurred but has been
suppressed), :filter (meaning the ld-pre-eval-filter terminated
ld), :missing-input (meaning that the specified input file is
missing, in the case that keyword :ld-missing-input-ok has a non-nil
value so that an error is avoided), or a cons pair whose first component is
the symbol :STOP-LD, which typically indicates that an error occurred
while the value of variable 'ld-error-action was :RETURN!.
See ld-error-action for details of this last case.
Subtopics
- Wormhole
- ld without state — a short-cut to a parallel universe
- Ld-skip-proofsp
- How carefully ACL2 processes your commands
- Ld-redefinition-action
- To allow redefinition without undoing
- Lp
- The Common Lisp entry to ACL2
- Ld-error-action
- Determines ld's response to an error
- Ld-history
- Saving and querying command history
- Guarantees-of-the-top-level-loop
- Guarantees provided by top-level evaluation
- Ld-post-eval-print
- Determines whether and how ld prints the result of evaluation
- Ld-keyword-aliases
- Abbreviation of some keyword commands
- Current-package
- The package used for reading and printing
- Ld-query-control-alist
- How to default answers to queries
- Ld-prompt
- Determines the prompt printed by ld
- Keyword-commands
- How keyword commands like :u and :pbt are processed
- Redef+
- System hacker's redefinition command
- Rebuild
- A convenient way to reconstruct your old state
- Prompt
- The prompt printed by ld
- Ld-pre-eval-print
- Determines whether ld prints the forms to be eval'd
- Calling-ld-in-bad-contexts
- Errors caused by calling ld in inappropriate contexts
- P!
- To pop up (at least) one level of ACL2's command loop
- Ld-pre-eval-filter
- Determines which forms ld evaluates
- Ld-error-triples
- Determines whether a form caused an error during ld
- Ld-evisc-tuple
- Determines whether ld suppresses details when printing
- Ld-verbose
- Determines whether ld prints ``ACL2 Loading ...''
- A!
- To return to the top-level of ACL2's command loop
- Default-print-prompt
- The default prompt printed by ld
- Reset-ld-specials
- Restores initial settings of the ld specials
- Ld-always-skip-top-level-locals
- Determines whether ld skips local top-level forms
- Ld-missing-input-ok
- Determine whether ld causes an error for a missing file
- Redef
- A common way to set ld-redefinition-action
- Redef!
- A common way to set ld-redefinition-action
- Redef-
- Turn off system hacker's redefinition command
- I-am-here
- A convenient marker for use with rebuild or ld
- Abort!
- To return to the top-level of ACL2's command loop
