#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 command.

def Std.Tactic.GuardMsgs.guardMsgsSpecElt : Lean.ParserDescr

Element that can be part of a #guard_msgs specification.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.GuardMsgs.guardMsgsSpec : Lean.ParserDescr

Specification for #guard_msgs command.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.GuardMsgs.guardMsgsCmd : Lean.ParserDescr

#guard_msgs captures the messages generated by another command and checks that they match the contents of the docstring attached to the #guard_msgs command.

Basic example:

/--
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 sorry. We can drop the warning completely with

#guard_msgs(error, drop warning) in
example : α := sorry

Syntax description:

#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:

• info, warning, error: intercept a message with the given severity level.
• all: intercept any message (so #guard_msgs in cmd and #guard_msgs (all) in cmd are equivalent).
• drop info, drop warning, 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.

For example, #guard_msgs (error, drop all) in cmd means to check warnings and then drop everything else.

Equations

• One or more equations did not get rendered due to their size.

inductive Std.Tactic.GuardMsgs.SpecResult : Type

The decision made by a specification for a message.

• 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.

def Std.Tactic.GuardMsgs.parseGuardMsgsSpec (spec? : Option (Lean.TSyntax `Std.Tactic.GuardMsgs.guardMsgsSpec)) : Lean.Elab.Command.CommandElabM (Lean.Message → Std.Tactic.GuardMsgs.SpecResult)

Parses a guardMsgsSpec.

• No specification: check everything.
• With a specification: interpret the spec, and if nothing applies pass it through.

Equations

• One or more equations did not get rendered due to their size.

structure Std.Tactic.GuardMsgs.GuardMsgFailure : Type

An info tree node corresponding to a failed #guard_msgs invocation, used for code action support.

• res : String

  The result of the nested command

instance Std.Tactic.GuardMsgs.instTypeNameGuardMsgFailure : TypeName Std.Tactic.GuardMsgs.GuardMsgFailure

Equations

• Std.Tactic.GuardMsgs.instTypeNameGuardMsgFailure = Std.Tactic.GuardMsgs.inst✝

def Std.Tactic.GuardMsgs.guardMsgsCodeAction : Std.CodeAction.CommandCodeAction

A code action which will update the doc comment on a #guard_msgs invocation.

Equations

• One or more equations did not get rendered due to their size.