Commit 2026-02-17 05:26 a9fd936a

View on Github →

feat(TacticAnalysis): verify grind? suggestions work (#33645) This PR adds a tactic analysis linter that runs grind? at proof steps, captures the "Try this:" suggestions, and verifies they actually close the goal when run. Two new options:

linter.tacticAnalysis.verifyGrind: verify grind? suggestions
linter.tacticAnalysis.verifyGrindSuggestions: verify grind? +suggestions Also adds runTacticCodeCapturingInfoTree to capture InfoTrees during tactic execution, enabling extraction of TryThis suggestions. 🤖 Prepared with Claude Code

Estimated changes

Modified Mathlib/Lean/ContextInfo.lean

added def Lean.Elab.ContextInfo.runCoreMCapturingInfoTree

added def Lean.Elab.ContextInfo.runMetaMCapturingInfoTree

added def Lean.Elab.ContextInfo.runTacticCapturingInfoTree

added def Lean.Elab.ContextInfo.runTacticCodeCapturingInfoTree

Modified Mathlib/Lean/Elab/InfoTree.lean

deleted def Lean.Elab.collectTryThisSuggestions

Modified Mathlib/Tactic/Says.lean

deleted def Mathlib.Tactic.Says.parseAsTacticSeq

Modified Mathlib/Tactic/TacticAnalysis.lean

Modified Mathlib/Tactic/TacticAnalysis/Declarations.lean

added def Mathlib.TacticAnalysis.verifyTryThisSuggestions

added def verifyGrind

added def verifyGrindSuggestions

Modified Mathlib/Util/ParseCommand.lean

added def Mathlib.GuardExceptions.parseAsTacticSeq

Modified MathlibTest/TacticAnalysis.lean