ld
's response to an error
Major Section: MISCELLANEOUS
Ld-error-action
is an ld
special (see ld). The accessor is
(ld-error-action state)
and the updater is
(set-ld-error-action val state)
. Ld-error-action
must be
:continue
, :return
, or :error
. The initial value of
ld-error-action
is :continue
, which means that the top-level
ACL2 command loop will not exit when an error is caused by
user-typein
. But the default value for ld-error-action
on
calls of ld
is :return
.
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-error-action
is one of them. If, while ld-error-triples
is t
, a
form evaluates to three results, the first of which is non-nil
and
the third of which is state
, an error is said to have occurred. If
an error occurs, ld
's action depends on ld-error-action
. If it is
:continue
, ld
just continues processing the forms in standard-oi
.
If it is :return
, ld
stops and returns as though it had emptied the
channel. If it is :error
, ld
stops and returns, signalling an error
to its caller.