Documentation

Std.Tactic.GuardMsgs

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

Element that can be part of a #guard_msgs specification.

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

    Specification for #guard_msgs command.

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

      #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.
      Instances For

        The decision made by a specification for a message.

        Instances For

          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.
          Instances For

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

            • res : String

              The result of the nested command

            Instances For

              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.
              Instances For