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

• tactics that emit messages, such as have?, extract_goal, or says;
• tactics that are in place to assert something, such as guard;
• tactics that allow to work on a specific goal, such as on_goal;
• "flow control" tactics, such as success_if_fail and related.

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

• conv is completely ignored by the linter.

• The linter does not enter a "sequence tactic": upon finding tac <;> [tac1, tac2, ...] the linter assumes that the tactic is doing something and does not recurse into each tac1, tac2, .... This is just for lack of an implementation: it may not be hard to do this.

• The tactic does not check the discharger for linear_combination, but checks linear_combination itself. The main reason is that skip is a common discharger tactic and the linter would then always fail whenever the user explicitly chose to pass skip as a discharger tactic.

TODO

• The linter seems to be silenced by set_option ... in: maybe it should enter ins?

Implementation notes

Yet another linter copied from the unreachableTactic linter!

opaque Mathlib.Linter.linter.unusedTactic : Lean.Option Bool

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

@[reducible, inline]

abbrev Mathlib.Linter.UnusedTactic.M (α : Type) : Type

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

Equations

• Mathlib.Linter.UnusedTactic.M = StateRefT' IO.RealWorld (Std.HashMap String.Range Lean.Syntax) IO

opaque Mathlib.Linter.UnusedTactic.allowedRef : IO.Ref (Std.HashSet Lean.SyntaxNodeKind)

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

def Mathlib.Linter.UnusedTactic.«command#allow_unused_tactic_» : Lean.ParserDescr

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

opaque Mathlib.Linter.UnusedTactic.ignoreTacticKindsRef : IO.Ref Lean.NameHashSet

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

def Mathlib.Linter.UnusedTactic.isIgnoreTacticKind (ignoreTacticKinds : Lean.NameHashSet) (k : Lean.SyntaxNodeKind) : Bool

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

Equations

• Mathlib.Linter.UnusedTactic.isIgnoreTacticKind ignoreTacticKinds (pre.str "quot") = ((pre.str "quot").components.contains `Conv || "slice".isPrefixOf (pre.str "quot").toString || true)
• Mathlib.Linter.UnusedTactic.isIgnoreTacticKind ignoreTacticKinds k = ((Lean.Name.components k).contains `Conv || "slice".isPrefixOf (Lean.Name.toString k) || ignoreTacticKinds.contains k)

def Mathlib.Linter.UnusedTactic.addIgnoreTacticKind (kind : Lean.SyntaxNodeKind) : IO Unit

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

Equations

• Mathlib.Linter.UnusedTactic.addIgnoreTacticKind kind = ST.Ref.modify Mathlib.Linter.UnusedTactic.ignoreTacticKindsRef fun (x : Lean.NameHashSet) => x.insert kind

@[specialize #[]]

partial def Mathlib.Linter.UnusedTactic.getTactics (ignoreTacticKinds : Lean.NameHashSet) (isTacKind : Lean.SyntaxNodeKind → Bool) (stx : Lean.Syntax) : Mathlib.Linter.UnusedTactic.M Unit

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

def Mathlib.Linter.UnusedTactic.getNames (mctx : Lean.MetavarContext) : List Lean.Name

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.

partial def Mathlib.Linter.UnusedTactic.eraseUsedTacticsList (trees : Lean.PersistentArray Lean.Elab.InfoTree) : Mathlib.Linter.UnusedTactic.M Unit

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

partial def Mathlib.Linter.UnusedTactic.eraseUsedTactics : Lean.Elab.InfoTree → Mathlib.Linter.UnusedTactic.M Unit

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

def Mathlib.Linter.UnusedTactic.unusedTacticLinter : Lean.Linter

The main entry point to the unused tactic linter.

Equations

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