Set-warnings-as-errors
Changing warnings to hard errors (and vice-versa)
It is common for ACL2 users not to notice warnings. That problem
can be avoided by using the utility set-warnings-as-errors to convert
warnings to errors. We start below with a general specification, followed by
example forms, a detailed specification, and finally an extended example.
General Form
The general form is
(set-warnings-as-errors flg types state)
where flg is t, :always, or nil and types is
either :all or a list of strings. The effect is to turn certain warnings into hard errors, aborting the computation in progress. Note
that set-warnings-as-errors is a function, so all arguments are
evaluated. Details are described in the section below entitled
“Detailed Specification”.
Example Forms
; When a [Subsume] or [Use] warning is to be printed, cause a hard error
; instead with a similar message.
(set-warnings-as-errors t '("Subsume" "Use") state)
; As above, but cause a hard error even if the warning is not to be printed,
; i.e., even if by default it would be suppressed as a warning because of
; prior use of set-inhibit-output-lst or set-inhibit-warnings.
(set-warnings-as-errors :always '("Subsume" "Use") state)
; Restore the treatment of [Use] warnings as warnings.
(set-warnings-as-errors nil '("Use") state)
; Treat a warning as a hard error, but only if the warning is to be printed
; (hence not suppressed by set-inhibit-output-lst or set-inhibit-warnings).
(set-warnings-as-errors t :all state)
; Treat a warning as a hard error, whether the warning is printed or not.
(set-warnings-as-errors :always :all state)
; Restore the default behavior, treating warnings as warnings, not errors.
(set-warnings-as-errors nil :all state)
Detailed Specification
- No warning whose type specified by constant
*uninhibited-warning-summaries* is converted to an error. Those types
are the ones that belong, with a case-insensitive check, to the list
("Uncertified" "Provisionally certified"
"Skip-proofs" "Defaxioms" "Ttags"
"Compiled file" "User-stobjs-modified"). This exception overrides all discussion
below.
- The behavior of warnings is affected for every warning type
specified by the types argument. When its value is :all, then all
warnings are affected. Otherwise the value of types is a list of warning
types (see set-inhibit-warnings): a true list of strings, each treated
as case-insensitive. Note that when the value is not :all, the existing
behavior for warning types is only changed for those in the value of
types.
- When flg is :always, then every warning specified by types
is converted to a hard error, which aborts the evaluation in progress. This
happens even if the warning is suppressed (by set-inhibit-output-lst
or set-inhibit-warnings).
- When flg is t, then when a warning specified by types is to
be printed, it is converted to a hard error, which aborts the evaluation in
progress. There is no error, however, if the warning is suppressed.
- When flg is nil, then every warning specified by types is
treated as a warning even if it had previously been treated as an error.
- When a warning of a given type (possibly nil type) is converted to a
hard error as specified above, then whether that error is printed is
controlled by the usual mechanism for suppressing error messages; see set-inhibit-er. Note that the error will still be signaled regardless of
whether the error message is thus suppressed.
- Previous evaluations of calls of set-warnings-as-errors are ignored
during certify-book and include-book. The handling of
warnings as errors is restored at the end of these operations to what it was
at the beginning.
Extended Example
ACL2 often prints warnings, often with a message that includes a
warning type. Here is a contrived example.
(defthm foo t
:hints (("Goal" :use car-cons))
:rule-classes nil)
ACL2 Warning [Use] in ( DEFTHM FOO ...): It is unusual to :USE the
formula of an enabled :REWRITE or :DEFINITION rule, so you may want
to consider disabling (:REWRITE CAR-CONS) in the hint provided for
Goal. See :DOC using-enabled-rules.
In the example above, the warning type is the string, "Use' which is
treated as case-insensitive; see set-inhibit-warnings. But maybe we
prefer that every such warning be converted to an error; after all, as the
warning suggests, we might want to disable the used rule first. It's easy to
miss a warning but not an error, so we might do the following.
(set-warnings-as-errors t '("use") state)
That modifies ACL2 behavior such that instead of the warning above, we get
the following error (after using :u to undo the effects of the
defthm event above).
HARD ACL2 ERROR [Use] in ( DEFTHM FOO ...): It is unusual to :USE
the formula of an enabled :REWRITE or :DEFINITION rule, so you may
want to consider disabling (:REWRITE CAR-CONS) in the hint provided
for Goal. See :DOC using-enabled-rules.
Note that this is a “hard” error: it aborts the computation in
progress.
Suppose however that we turn off the warning by evaluating either of the
following two forms.
(set-inhibit-output-lst '(warning proof-tree))
; OR
(set-inhibit-warnings "use")
After evaluating either (or both) of these forms, the defthm form
above completes with no warnings or errors. That's because there was no
warning to print, and the flg value of t only has an effect for
warnings that are printed. If we want errors to occur even for warnings whose
printing is suppressed, we should use the flg value, :always.
(set-warnings-as-errors :always '("use") state)
; OR
(set-warnings-as-errors :always :all state)
