Tactic linters

This file defines passes to run from the tactic analysis framework.

def Mathlib.TacticAnalysis.terminalReplacement (oldTacticName newTacticName : String) (oldTacticKind : Lean.SyntaxNodeKind) (newTactic : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → Lean.Syntax → Lean.Elab.Command.CommandElabM (Lean.TSyntax `tactic)) (reportFailure : Bool := true) (reportSuccess reportSlowdown : Bool := false) (maxSlowdown : Float := 1) : Config

Define a pass that tries replacing one terminal tactic with another.

newTacticName is a human-readable name for the tactic, for example "linarith". This can be used to group messages together, so that ring, ring_nf, ring1, ... all produce the same message.

oldTacticKind is the SyntaxNodeKind for the tactic's main parser, for example Mathlib.Tactic.linarith.

newTactic stx goal selects the new tactic to try, which may depend on the old tactic invocation in stx and the current goal.

def Mathlib.TacticAnalysis.grindReplacementWith (tacticName : String) (tacticKind : Lean.SyntaxNodeKind) (extractArgs : Lean.Syntax → Option (Lean.Syntax.TSepArray `term ",") := fun (x : Lean.Syntax) => none) (reportFailure : Bool := true) (reportSuccess reportSlowdown : Bool := false) (maxSlowdown : Float := 1) : Config

Define a pass that tries replacing a specific tactic with grind.

tacticName is a human-readable name for the tactic, for example "linarith". This can be used to group messages together, so that ring, ring_nf, ring1, ... all produce the same message.

tacticKind is the SyntaxNodeKind for the tactic's main parser, for example Mathlib.Tactic.linarith.

If extractArgs is provided, it extracts term arguments from the original tactic (e.g., linarith [X, Y]) and passes them to grind (e.g., grind [X, Y]). Local hypotheses are filtered out since grind uses them automatically.

opaque linter.tacticAnalysis.regressions.linarithToGrind : Lean.Option Bool

Debug grind by identifying places where it does not yet supersede linarith.

def linarithToGrindRegressions : Mathlib.TacticAnalysis.Config

Debug grind by identifying places where it does not yet supersede linarith.

opaque linter.tacticAnalysis.regressions.ringToGrind : Lean.Option Bool

Debug grind by identifying places where it does not yet supersede ring.

def ringToGrindRegressions : Mathlib.TacticAnalysis.Config

Debug grind by identifying places where it does not yet supersede ring.

opaque linter.tacticAnalysis.regressions.omegaToLia : Lean.Option Bool

Debug lia by identifying places where it does not yet supersede omega.

def omegaToLiaRegressions : Mathlib.TacticAnalysis.Config

Debug lia by identifying places where it does not yet supersede omega.

opaque linter.tacticAnalysis.omegaToLia : Lean.Option Bool

Report places where omega can be replaced by lia.

def omegaToLia : Mathlib.TacticAnalysis.Config

Report places where omega can be replaced by lia.

opaque linter.tacticAnalysis.rwMerge : Lean.Option Bool

Suggest merging two adjacent rw tactics if that also solves the goal.

def Mathlib.TacticAnalysis.rwMerge : Config

Suggest merging two adjacent rw tactics if that also solves the goal.

opaque linter.tacticAnalysis.mergeWithGrind : Lean.Option Bool

Suggest merging tac; grind into just grind if that also solves the goal.

def Mathlib.TacticAnalysis.mergeWithGrind : Config

Suggest merging tac; grind into just grind if that also solves the goal.

opaque linter.tacticAnalysis.terminalToGrind : Lean.Option Bool

Suggest replacing a sequence of tactics with grind if that also solves the goal.

def Mathlib.TacticAnalysis.terminalToGrind : Config

Suggest replacing a sequence of tactics with grind if that also solves the goal.

opaque linter.tacticAnalysis.tryAtEachStep.fraction : Lean.Option ℕ

When running the "tryAtEachStep" tactic analysis linters, only run on a fraction 1/n of the goals found in the library.

This is useful for running quick benchmarks.

opaque linter.tacticAnalysis.tryAtEachStep.showTiming : Lean.Option Bool

Whether to show timing information in "tryAtEachStep" tactic analysis output.

When true (default), messages include elapsed time like (23ms). Set to false in tests to avoid non-deterministic output.

opaque linter.tacticAnalysis.tryAtEachStep.selfReplacements : Lean.Option Bool

Whether to report when a tactic can be replaced with itself.

When true (default), all successful replacements are reported, including when the suggested tactic matches the existing proof. When false, self-replacements are suppressed.

def Mathlib.TacticAnalysis.tryAtEachStepCore (tac : Lean.Syntax → Lean.MVarId → Lean.Elab.Command.CommandElabM (Lean.TSyntax `tactic)) (label : Option String := none) : Config

Run a tactic at each proof step, with optional timing.

label is an optional human-readable name for output. If none, the tactic syntax is used.

Reports elapsed time in milliseconds for each successful replacement when linter.tacticAnalysis.tryAtEachStep.showTiming is true.

When linter.tacticAnalysis.tryAtEachStep.selfReplacements is false, cases where the suggested tactic matches the existing proof are suppressed.

def Mathlib.TacticAnalysis.tryAtEachStep (tac : Lean.Syntax → Lean.MVarId → Lean.Elab.Command.CommandElabM (Lean.TSyntax `tactic)) : Config

Run a tactic at each proof step. See tryAtEachStepCore for details.

def Mathlib.TacticAnalysis.tryAtEachStepFromStrings (label tacticStr : String) : Config

Run a tactic (given as a string) at each proof step, with optional timing.

label is the human-readable name shown in output (e.g., "grind"). tacticStr is the tactic syntax as a string (e.g., "grind +suggestions"). Tactic sequences like "simp; grind" are also supported.

Reports elapsed time in milliseconds for each successful replacement when linter.tacticAnalysis.tryAtEachStep.showTiming is true. To limit tactic runtime, use set_option maxHeartbeats N in the build command.

When linter.tacticAnalysis.tryAtEachStep.selfReplacements is false, cases where the suggested tactic matches the existing proof are suppressed.

def Mathlib.TacticAnalysis.tryAtEachStepFromEnvImpl : Config

Run a custom tactic at each proof step, configured via environment variables.

Reads from environment variables:

• TRY_AT_EACH_STEP_TACTIC: Tactic syntax to try (e.g., "grind +suggestions") - required
• TRY_AT_EACH_STEP_LABEL: Human-readable label for output (optional, defaults to tactic)

If TRY_AT_EACH_STEP_TACTIC is missing, this linter does nothing.

To enable, add to the mathlibOnlyLinters array in lakefile.lean:

⟨`linter.tacticAnalysis.tryAtEachStepFromEnv, true⟩,

Then run with the environment variable:

TRY_AT_EACH_STEP_TACTIC="grind +suggestions" lake build Mathlib

This generic entry point is used by the hammer-bench benchmarking tool (https://github.com/leanprover-community/hammer-bench) to test arbitrary tactics without requiring Mathlib code changes for each new tactic variant.

opaque linter.tacticAnalysis.tryAtEachStepGrind : Lean.Option Bool

Run grind at every step in proofs, reporting where it succeeds.

def tryAtEachStepGrind : Mathlib.TacticAnalysis.Config

Run grind at every step in proofs, reporting where it succeeds.

opaque linter.tacticAnalysis.tryAtEachStepSimpAll : Lean.Option Bool

Run simp_all at every step in proofs, reporting where it succeeds.

def tryAtEachStepSimpAll : Mathlib.TacticAnalysis.Config

Run simp_all at every step in proofs, reporting where it succeeds.

opaque linter.tacticAnalysis.tryAtEachStepAesop : Lean.Option Bool

Run aesop at every step in proofs, reporting where it succeeds.

def tryAtEachStepAesop : Mathlib.TacticAnalysis.Config

Run aesop at every step in proofs, reporting where it succeeds.

opaque linter.tacticAnalysis.tryAtEachStepGrindSuggestions : Lean.Option Bool

Run grind +suggestions at every step in proofs, reporting where it succeeds.

def tryAtEachStepGrindSuggestions : Mathlib.TacticAnalysis.Config

Run grind +suggestions at every step in proofs, reporting where it succeeds.

opaque linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions : Lean.Option Bool

Run simp_all? +suggestions at every step in proofs, reporting where it succeeds.

def tryAtEachStepSimpAllSuggestions : Mathlib.TacticAnalysis.Config

Run simp_all? +suggestions at every step in proofs, reporting where it succeeds.

opaque linter.tacticAnalysis.tryAtEachStepFromEnv : Lean.Option Bool

Run a custom tactic at every step in proofs, configured via environment variables.

Set TRY_AT_EACH_STEP_TACTIC to the tactic syntax to try (required). Set TRY_AT_EACH_STEP_LABEL to the label for output messages (optional, defaults to tactic).

def tryAtEachStepFromEnv : Mathlib.TacticAnalysis.Config

Run a custom tactic at every step in proofs, configured via environment variables.

Set TRY_AT_EACH_STEP_TACTIC to the tactic syntax to try (required). Set TRY_AT_EACH_STEP_LABEL to the label for output messages (optional, defaults to tactic).

opaque linter.tacticAnalysis.introMerge : Lean.Option Bool

Suggest merging two adjacent intro tactics which don't pattern match.

def Mathlib.TacticAnalysis.introMerge : Config

Suggest merging two adjacent intro tactics which don't pattern match.

def Mathlib.TacticAnalysis.verifyTryThisSuggestions (tac : Lean.Syntax → Lean.MVarId → Lean.Elab.Command.CommandElabM (Lean.TSyntax `tactic)) (label : String) : Config

Verify that TryThis suggestions from a tactic actually work.

Runs the given tactic at each proof step, captures any "Try this:" suggestions, then re-runs the suggested tactic to verify it succeeds. Only reports failures (where the suggestion doesn't close the goal).

opaque linter.tacticAnalysis.verifyGrind : Lean.Option Bool

Verify that grind? suggestions actually work.

def verifyGrind : Mathlib.TacticAnalysis.Config

Verify that grind? suggestions actually work.

opaque linter.tacticAnalysis.verifyGrindSuggestions : Lean.Option Bool

Verify that grind? +suggestions suggestions actually work.

def verifyGrindSuggestions : Mathlib.TacticAnalysis.Config

Verify that grind? +suggestions suggestions actually work.