LD-ERROR-ACTION

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.