/-- ... -/ #guard_msgs in cmd
captures the messages generated by the command cmd
and checks that they match the contents of the docstring.
Basic example:
/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x
This checks that there is such an error and then consumes the message.
By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings:
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
or only errors
#guard_msgs(error) in
example : α := sorry
In the previous example, since warnings are not captured there is a warning on sorry
.
We can drop the warning completely with
#guard_msgs(error, drop warning) in
example : α := sorry
In general, #guard_msgs
accepts a comma-separated list of configuration clauses in parentheses:
#guard_msgs (configElt,*) in cmd
By default, the configuration list is (check all, whitespace := normalized, ordering := exact)
.
Message filters select messages by severity:
info
,warning
,error
: (non-trace) messages with the given severity level.trace
: trace messagesall
: all messages.
The filters can be prefixed with the action to take:
check
(the default): capture and check the messagedrop
: drop the messagepass
: let the message pass through
If no filter is specified, check all
is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit pass all
at the end.
Whitespace handling (after trimming leading and trailing whitespace):
whitespace := exact
requires an exact whitespace match.whitespace := normalized
converts all newline characters to a space before matching (the default). This allows breaking long lines.whitespace := lax
collapses whitespace to a single space before matching.
Message ordering:
ordering := exact
uses the exact ordering of the messages (the default).ordering := sorted
sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering.
For example, #guard_msgs (error, drop all) in cmd
means to check warnings and drop
everything else.
The command elaborator has special support for #guard_msgs
for linting.
The #guard_msgs
itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for all top-level commands,
which would include #guard_msgs
itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if #guard_msgs
is not present.
Equations
- One or more equations did not get rendered due to their size.