Set-inhibit-warnings
Control warnings
Examples:
(set-inhibit-warnings "theory" "use")
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-warnings! for a corresponding non-local event.
Indeed, (set-inhibit-warnings ...) is equivalent to (local
(set-inhibit-warnings! ...)).
General Form:
(set-inhibit-warnings string1 string2 ...)
where each string is considered without regard to case. This macro is is
essentially (local (table inhibit-warnings-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-warnings event.
ACL2 prints warnings that may, from time to time, seem excessive to
experienced users. Each warning is ``labeled'' with a string identifying the
type of warning. Consider for example
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE ....
Here, the label is "Use". The argument list for
set-inhibit-warnings is a list of such labels, each of which is a string.
Any warning is suppressed if its label is a member of this list, where case is
ignored. Thus, for example, the warning above will not be printed after a
call of set-inhibit-warnings that contains the string, "Use" (or
any string that is string-equal to "Use", such as "use"
or "USE"). In summary: the effect of this event is to suppress any
warning whose label is a member of the given argument list, where case is
ignored.
The list of currently inhibited warnings is the list of keys in the table named inhibit-warnings-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-warnings-table (w state)). Of
course, if warnings are inhibited overall — see set-inhibit-output-lst — then this value is entirely irrelevant.
See toggle-inhibit-warning for a way to add or remove a single
warning string.
