Tactic linters

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

def tacticLia : Lean.ParserDescr

lia is an alias for the cutsat tactic, which solves linear integer arithmetic goals.

Equations

• tacticLia = Lean.ParserDescr.node `tacticLia 1024 (Lean.ParserDescr.nonReservedSymbol "lia" false)

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.

Equations

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

def Mathlib.TacticAnalysis.grindReplacementWith (tacticName : String) (tacticKind : Lean.SyntaxNodeKind) (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.

Equations

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

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.

Equations

• linarithToGrindRegressions = Mathlib.TacticAnalysis.grindReplacementWith "linarith" `Mathlib.Tactic.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.

Equations

• ringToGrindRegressions = Mathlib.TacticAnalysis.grindReplacementWith "ring" `Mathlib.Tactic.RingNF.ring

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

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

def omegaToCutsatRegressions : Mathlib.TacticAnalysis.Config

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

Equations

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

opaque linter.tacticAnalysis.omegaToCutsat : Lean.Option Bool

Report places where omega can be replaced by lia.

def omegaToCutsat : Mathlib.TacticAnalysis.Config

Report places where omega can be replaced by lia.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

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.

Equations

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

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.

Equations

• Mathlib.TacticAnalysis.tryAtEachStep tac = Mathlib.TacticAnalysis.tryAtEachStepCore tac

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

• tryAtEachStepFromEnv = Mathlib.TacticAnalysis.tryAtEachStepFromEnvImpl

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.

Equations

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