ld prints the result of evaluation
Major Section: MISCELLANEOUS
Ld-post-eval-print is an ld special (see ld). The accessor is
(ld-post-eval-print state) and the updater is
(set-ld-post-eval-print val state). Ld-post-eval-print must be
either t, nil, or :command-conventions. The initial value of
ld-post-eval-print is :command-conventions.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-post-eval-print is one of them. If this global variable is t,
ld prints the result. In the case of a form that produces a multiple
value, ld prints the list containing all the values (which, logically
speaking, is what the form returned). If ld-post-eval-print is nil,
ld does not print the values. This is most useful when ld is
used to load a previously processed file.
Finally, if ld-post-eval-print is :command-conventions and also
ld-error-triples is t, then ld prints the result but treats
``error triples'' specially. An ``error triple'' (see error-triples) is a
result, (mv erp val state), that consists of two ordinary values and
state. Many ACL2 functions use such triples to signal errors. The
convention is that if erp (the first value) is nil, then the function
is returning val (the second value) as its conventional single result and
possibly side-effecting state (as with some output). If erp is
t, then an error has been caused, val is irrelevant and the error
message has been printed in the returned state. Example ACL2 functions
that follow this convention include defun and in-package. If
such ``error producing'' functions are evaluated while ld-post-eval-print
is set to t, then you would see them producing lists of length 3. This
is disconcerting to users accustomed to Common Lisp (where these functions
produce single results but sometimes cause errors or side-effect state).
For more information about error triples, see programming-with-state.
When ld-post-eval-print is :command-conventions and a form produces
an error triple (mv erp val state) as its value, ld prints nothing
if erp is non-nil and otherwise ld prints just val.
Because it is a misrepresentation to suggest that just one result was
returned, ld prints the value of the global variable
'triple-print-prefix before printing val. 'triple-print-prefix
is initially " ", which means that when non-erroneous error triples are
being abbreviated to val, val appears one space off the left margin
instead of on the margin.
In addition, when ld-post-eval-print is :command-conventions and the
value component of an error triple is the keyword :invisible then
ld prints nothing. This is the way certain commands (e.g.,
:pc) appear to return no value.
By printing nothing when an error has been signalled, ld makes it
appear that the error (whose message has already appeared in state) has
``thrown'' the computation back to load without returning a value. By
printing just val otherwise, we suppress the fact that state has
possibly been changed.
