def Lean.Elab.Tactic.InfoTrees.elabInfoTrees : Command.CommandElab

/-- ... -/ #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 (all, whitespace := normalized, ordering := exact).

Message filters (processed in left-to-right order):

• info, warning, error: capture messages with the given severity level.
• all: capture all messages (the default).
• drop info, drop warning, drop error: drop messages with the given severity level.
• drop all: drop every message.

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.