Ld-post-eval-print
Determines whether and how ld prints the result of evaluation
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. Note that the ACL2 top-level loop (see lp) results from
an invocation of ld.
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-triple)
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 not nil, 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.
