Documentation

Mathlib.Tactic.Linter.UnusedTactic

The unused tactic linter #

The unused linter makes sure that every tactic call actually changes something.

The inner workings of the linter are as follows.

The linter inspects the goals before and after each tactic execution. If they are not identical, the linter is happy. If they are identical, then the linter checks if the tactic is whitelisted. Possible reason for whitelisting are

The only tactic that has a bespoke criterion is swap_var: the reason is that the only change that swap_var has is to relabel the usernames of local declarations. Thus, to check that swap_var was used, so we inspect the names of all the local declarations before and after and see if there is some change.

Notable exclusions #

TODO #

Implementation notes #

Yet another linter copied from the unreachableTactic linter!

The unused tactic linter makes sure that every tactic call actually changes something.

@[reducible, inline]

The monad for collecting the ranges of the syntaxes that do not modify any goal.

Equations
Instances For

    Parsers allowed to not change the tactic state. This can be increased dynamically, using #allow_unused_tactic.

    #allow_unused_tactic takes an input a space-separated list of identifiers. These identifiers are then allowed by the unused tactic linter: even if these tactics do not modify goals, there will be no warning emitted. Note: for this to work, these identifiers should be the SyntaxNodeKind of each tactic.

    For instance, you can allow the done and skip tactics using

    #allow_unused_tactic Lean.Parser.Tactic.done Lean.Parser.Tactic.skip
    

    Notice that you should use the SyntaxNodeKind of the tactic.

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

      A list of blacklisted syntax kinds, which are expected to have subterms that contain unevaluated tactics.

      Is this a syntax kind that contains intentionally unused tactic subterms?

      Equations
      Instances For

        Adds a new syntax kind whose children will be ignored by the unusedTactic linter. This should be called from an initialize block.

        Equations
        Instances For
          @[specialize #[]]

          Accumulates the set of tactic syntaxes that should be evaluated at least once.

          getNames mctx extracts the names of all the local declarations implied by the MetavarContext mctx.

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

            Search for tactic executions in the info tree and remove the syntax of the tactics that changed something.

            Search for tactic executions in the info tree and remove the syntax of the tactics that changed something.

            The main entry point to the unused tactic linter.

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