Control the error output
Examples: (set-inhibit-er-soft "translate" "failure")
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded. It
is local to the book or encapsulate form in which it occurs;
see set-inhibit-er-soft! for a corresponding non-local event.
General Form: (set-inhibit-er-soft string1 string2 ...)
where each string is considered without regard to case. This macro is is
ACL2 prints errors that are generally important to see. This utility is appropriate for situations where one prefers not to see all error messages. to. Individual ``labeled'' error output can be silenced. Consider for example
ACL2 Error [Failure] in ( DEFUN FOO ...): See :DOC failure.
Here, the label is "Failure". The argument list for
At this time, many error messages are printed without a label, for example (as of this writing) the following.
ACL2 !>(+ x 3) ACL2 Error in TOP-LEVEL: Global variables, such as X, are not allowed. See :DOC ASSIGN and :DOC @. ACL2 !>
These can only be suppressed by turning off all error output; see set-inhibit-output-lst. Feel free to ask the ACL2 implementors to add
labels; for example, you might ask for a label in the example above (which
HARD ACL2 ERROR in SET-GAG-MODE: Unknown set-gag-mode argument, ABC
The list of currently inhibited error types is the list of keys in the
See toggle-inhibit-er-soft for a way to add or remove a single string.