#guard_msgs and #guard_panic commands for testing commands

This module defines commands to test that other commands produce expected messages:

• #guard_msgs: tests that a command produces exactly the expected messages
• #guard_panic: tests that a command produces a panic message (without checking the exact text)

See the docstrings on the individual commands.

opaque guard_msgs.diff : Lean.Option Bool

inductive Lean.Elab.Tactic.GuardMsgs.FilterSpec : Type

The decision made by a specification for a message.

• check : FilterSpec

  Capture the message and check it matches the docstring.

• drop : FilterSpec

  Drop the message and delete it.

• pass : FilterSpec

  Do not capture the message.

inductive Lean.Elab.Tactic.GuardMsgs.WhitespaceMode : Type

The method to use when normalizing whitespace, after trimming.

• exact : WhitespaceMode

  Exact equality.

• normalized : WhitespaceMode

  Equality after normalizing newlines into spaces.

• lax : WhitespaceMode

  Equality after collapsing whitespace into single spaces.

inductive Lean.Elab.Tactic.GuardMsgs.MessageOrdering : Type

Method to use when combining multiple messages.

• exact : MessageOrdering

  Use the exact ordering of the produced messages.

• sorted : MessageOrdering

  Sort the produced messages.

structure Lean.Elab.Tactic.GuardMsgs.GuardMsgsSpec : Type

The specification options for #guard_msgs. The default field values provide the default behavior of #guard_msgs.

• filterFn : Message → FilterSpec

  Method for deciding whether and how to filter messages; see FilterSpec.

• whitespace : WhitespaceMode

  Method to use when normalizing whitespace, after trimming; see WhitespaceMode.

• ordering : MessageOrdering

  Method to use when combining multiple messages; see MessageOrdering.

• reportPositions : Bool

  Whether to report position information.

• substring : Bool

  Whether to check for substring containment instead of exact match.

def Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsFilterAction (action? : Option (TSyntax `Lean.guardMsgsFilterAction)) : Command.CommandElabM FilterSpec

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsFilterAction action? = pure Lean.Elab.Tactic.GuardMsgs.FilterSpec.check

def Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsFilterSeverity : TSyntax `Lean.guardMsgsFilterSeverity → Command.CommandElabM (Message → Bool)

Equations

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

def Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsSpec (spec? : Option (TSyntax `Lean.guardMsgsSpec)) : Command.CommandElabM GuardMsgsSpec

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.
• Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsSpec spec? = pure { }

structure Lean.Elab.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 Lean.Elab.Tactic.GuardMsgs.instTypeNameGuardMsgFailure : TypeName GuardMsgFailure

Equations

• Lean.Elab.Tactic.GuardMsgs.instTypeNameGuardMsgFailure = Lean.Elab.Tactic.GuardMsgs.inst✝

def Lean.Elab.Tactic.GuardMsgs.revealTrailingWhitespace (s : String) : String

Makes trailing whitespace visible and protects them against trimming by the editor, by appending the symbol ⏎ to such a line (and also to any line that ends with such a symbol, to avoid ambiguities in the case the message already had that symbol).

Equations

• Lean.Elab.Tactic.GuardMsgs.revealTrailingWhitespace s = ((s.replace "⏎\n" "⏎⏎\n").replace "\t\n" "\t⏎\n").replace " \n" " ⏎\n"

def Lean.Elab.Tactic.GuardMsgs.removeTrailingWhitespaceMarker (s : String) : String

Equations

• Lean.Elab.Tactic.GuardMsgs.removeTrailingWhitespaceMarker s = s.replace "⏎\n" "\n"

def Lean.Elab.Tactic.GuardMsgs.WhitespaceMode.apply (mode : WhitespaceMode) (s : String) : String

Applies a whitespace normalization mode.

Equations

• Lean.Elab.Tactic.GuardMsgs.WhitespaceMode.exact.apply s = s
• Lean.Elab.Tactic.GuardMsgs.WhitespaceMode.normalized.apply s = s.replace "\n" " "
• Lean.Elab.Tactic.GuardMsgs.WhitespaceMode.lax.apply s = " ".toSlice.intercalate (Std.Iter.filter (fun (x : String.Slice) => !x.isEmpty) (s.split Char.isWhitespace)).toList

def Lean.Elab.Tactic.GuardMsgs.MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List String

Applies a message ordering mode.

Equations

• Lean.Elab.Tactic.GuardMsgs.MessageOrdering.exact.apply msgs = msgs
• Lean.Elab.Tactic.GuardMsgs.MessageOrdering.sorted.apply msgs = (msgs.toArray.qsort fun (x1 x2 : String) => decide (x1 < x2)).toList

def Lean.Elab.Tactic.GuardMsgs.runAndCollectMessages (cmd : Syntax) : Command.CommandElabM MessageLog

Runs a command and collects all messages (sync and async) it produces. Clears the snapshot tasks after collection. Returns the collected messages.

Equations

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

def Lean.Elab.Tactic.GuardMsgs.elabGuardMsgs : Command.CommandElab

Equations

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

def Lean.Elab.Tactic.GuardMsgs.guardMsgsCodeAction : 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.
• Lean.Elab.Tactic.GuardMsgs.guardMsgsCodeAction x✝² x✝¹ x✝ node = pure #[]

def Lean.Elab.Tactic.GuardMsgs.elabGuardPanic : Command.CommandElab

Equations

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