		Search-engine friendly clone of the ACL2 documentation.

Set-inhibit-er

Control the error output

Examples:
(set-inhibit-er "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! for a corresponding non-local event. Indeed, (set-inhibit-er ...) is equivalent to (local (set-inhibit-er! ...)).

General Form:
(set-inhibit-er string1 string2 ...)

where each string is considered without regard to case. This macro is is essentially (local (table inhibit-er-table nil 'alist :clear)), where alist pairs each supplied string with nil: that is, alist is (pairlis$ lst nil) where lst is the list of strings supplied. This macro is an event (see table), but no output results from a set-inhibit-er event.

ACL2 prints errors that are generally important to see. This utility is appropriate for situations where one prefers not to see all error messages. 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 set-inhibit-er is a list of such labels, each of which is a string. Any error message is suppressed if its label is a member of this list, where case is ignored. Thus, for example, the error output above will be avoided after a call of set-inhibit-er that contains the string, "Failure" (or any string that is string-equal to "Failure", such as "failure" or "FAILURE"). In summary: the effect of this event is to suppress any error output whose label is a member of the given argument list, where case is ignored.

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 could be "Globals" or "Global-variables").

Note that set-inhibit-er has no effect on the value(s) returned by an expression (excepting the ACL2 state since it formally includes output).

The list of currently inhibited error types is the list of keys in the table named inhibit-er-table. (The values in the table are irrelevant.) One way to get that value is to get the result from evaluating the following form: (table-alist 'inhibit-er-table (w state)). Of course, if error output is inhibited overall — see set-inhibit-output-lst — then this value is entirely irrelevant.

See toggle-inhibit-er for a way to add or remove a single string.