Lean4
@[tacticAnalysis linter.tacticAnalysis.terminalToGrind, inherit_doc linter.tacticAnalysis.terminalToGrind]
def terminalToGrind : TacticAnalysis.Config where
run
seq := do
let threshold :=
3
-- `replaced` will hold the terminal tactic sequence that can be replaced with `grind`.
-- We prepend each tactic in turn, starting with the last.
let mut replaced : List (TSyntax `tactic) := []
let mut success := false
let mut oldHeartbeats := 0
let mut newHeartbeats :=
0
-- We iterate through the tactic sequence in reverse, checking at each tactic if the goal is
-- already solved by `grind` and if so pushing that tactic onto `replaced`.
-- By repeating this until `grind` fails for the first time, we get a terminal sequence
-- of replaceable tactics.
for (ctx, i) in seq.reverse do
if replaced.length >= threshold - 1 && i.stx.getKind != ``Lean.Parser.Tactic.grind then
if let [goal] := i.goalsBefore then
-- Count the heartbeats of the original tactic sequence, verifying that this indeed
-- closes the goal like it does in userspace.
let suffix := ⟨i.stx⟩ :: replaced
let seq ← `(tactic| $suffix.toArray;*)
let (oldGoals, heartbeats) ←
withHeartbeats <|
try
ctx.runTacticCode i goal seq
catch _e =>
pure [goal]
if !oldGoals.isEmpty then
logWarningAt i.stx m! "Original tactics failed to solve the goal: {seq}"
oldHeartbeats := heartbeats
let tac ← `(tactic| grind)
let (newGoals, heartbeats) ←
withHeartbeats <|
try
ctx.runTacticCode i goal tac
catch _e =>
pure [goal]
newHeartbeats := heartbeats
if newGoals.isEmpty then
success := true
else
break
else
break
replaced := ⟨i.stx⟩ :: replaced
if h : replaced.length >= threshold ∧ success then
let stx := replaced[0]
let seq ← `(tactic| $replaced.toArray;*)
logWarningAt stx m! "replace the proof with 'grind': {seq}"
if oldHeartbeats * 2 < newHeartbeats then
logWarningAt stx m! "'grind' is slower than the original: {oldHeartbeats } -> {newHeartbeats}"
