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

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

def Mathlib.Linter.UnusedTactic.allowUnusedTactic : Lean.ParserDescr

allow_unused_tactic takes as 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

This change is global and persistent across imports. For a file-local or scoped change, use local allow_unused_tactic or scoped allow_unused_tactic, respectively.

The command #show_kind tac may help to find the SyntaxNodeKind.

Equations

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

def Mathlib.Linter.UnusedTactic.hashStx : Lean.ParserDescr

#allow_unused_tactic is deprecated in favour of allow_unused_tactic

Equations

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

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

#show_kind tac takes as input the syntax of a tactic and returns the SyntaxNodeKind at the head of the tactic syntax tree.

The input syntax needs to parse, though it can be extremely elided. For instance, to see the SyntaxNodeKind of the refine tactic, you could use

#show_kind refine _

The trailing underscore _ makes the syntax valid, since refine expects something else.

Equations

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

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") = (true || ignoreTacticKinds.contains (pre.str "quot"))
• Mathlib.Linter.UnusedTactic.isIgnoreTacticKind ignoreTacticKinds k = (false || ignoreTacticKinds.contains k)

def Mathlib.Linter.UnusedTactic.addIgnoreTacticKind (kind : Lean.SyntaxNodeKind) : BaseIO 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