#guard_msgs command for testing commands
This module defines a command to test that another command produces the expected messages.
See the docstring on the
#guard_msgs captures the messages generated by another command and checks that they
match the contents of the docstring attached to the
/-- error: unknown identifier 'x' -/ #guard_msgs in example : α := x
This checks that there is such an error and then consumes the message entirely.
By default, the command intercepts all messages, but there is a way to specify which types of messages to consider. 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 this last example, since the message is not intercepted there is a warning on
We can drop the warning completely with
#guard_msgs(error, drop warning) in example : α := sorry
#guard_msgs (drop? info|warning|error|all,*)? in cmd
If there is no specification,
#guard_msgs intercepts all messages.
Otherwise, if there is one, the specification is considered in left-to-right order, and the first
that applies chooses the outcome of the message:
error: intercept a message with the given severity level.
all: intercept any message (so
#guard_msgs in cmdand
#guard_msgs (all) in cmdare equivalent).
drop error: intercept a message with the given severity level and then drop it. These messages are not checked.
drop all: intercept a message and drop it.
#guard_msgs (error, drop all) in cmd means to check warnings and then drop
- check: Std.Tactic.GuardMsgs.SpecResult
Capture the message and check it matches the docstring.
- drop: Std.Tactic.GuardMsgs.SpecResult
Drop the message and delete it.
- passthrough: Std.Tactic.GuardMsgs.SpecResult
Do not capture the message.
The decision made by a specification for a message.
- No specification: check everything.
- With a specification: interpret the spec, and if nothing applies pass it through.