feat: config options at finish

This PR adds support for configuration options at `finish` and `finish?`.

Author: leodemoura

src/Init/Grind/Interactive.lean

@@ -129,10 +129,10 @@ syntax (name := casesTrace) "cases?" grindFilter : grind
 syntax (name := done) "done" : grind
 
 /-- `finish` tries to close the current goal using `grind`'s default strategy -/
-syntax (name := finish) "finish" : grind
+syntax (name := finish) "finish" ppSpace configItem* : grind
 
 /-- `finish?` tries to close the current goal using `grind`'s default strategy and suggests a tactic script. -/
-syntax (name := finishTrace) "finish?" : grind
+syntax (name := finishTrace) "finish?" ppSpace configItem* : grind
 
 /--
 The `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -82,14 +82,16 @@ def evalGrindSeq : GrindTactic := fun stx =>
 
 open Meta Grind
 
-@[builtin_grind_tactic finish] def evalFinish : GrindTactic := fun _ => do
-  let goal ← getMainGoal
-  if let some goal ← liftGrindM <| solve goal then
-    let params := (← read).params
-    let result ← liftGrindM do mkResult params (some goal)
-    throwError "`finish` failed\n{← result.toMessageData}"
-  else
-    replaceMainGoal []
+@[builtin_grind_tactic finish] def evalFinish : GrindTactic := fun stx => withMainContext do
+  let `(grind| finish $[$configItems]*) := stx | throwUnsupportedSyntax
+  withConfigItems configItems do
+    let goal ← getMainGoal
+    if let some goal ← liftGrindM <| solve goal then
+      let params := (← read).params
+      let result ← liftGrindM do mkResult params (some goal)
+      throwError "`finish` failed\n{← result.toMessageData}"
+    else
+      replaceMainGoal []
 
 /--
 Helper function to executing "check" tactics that return a flag indicating
@@ -432,10 +434,7 @@ where
 
 @[builtin_grind_tactic setConfig] def elabSetConfig : GrindTactic := fun stx => do
   let `(grind| set_config $[$items:configItem]* in $seq:grindSeq) := stx | throwUnsupportedSyntax
-  let config := (← read).ctx.config
-  let config ← elabConfigItems config items
-  withReader (fun c => { c with ctx.config := config }) do
-    evalGrindTactic seq
+  withConfigItems items do evalGrindTactic seq
 
 @[builtin_grind_tactic mbtc] def elabMBTC : GrindTactic := fun _ => do
   liftGoalM do

src/Lean/Elab/Tactic/Grind/Config.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.CoreM
+public import Lean.Elab.Tactic.Grind.Basic
 meta import Lean.Elab.Tactic.ConfigSetter
 public section
 namespace Lean.Elab.Tactic.Grind
@@ -29,4 +29,13 @@ def elabConfigItems (init : Grind.Config) (items : Array (TSyntax `Lean.Parser.T
     | _ => throwErrorAt item "unexpected configuration option"
   return config
 
+def withConfigItems (items : Array (TSyntax `Lean.Parser.Tactic.configItem))
+    (k : GrindTacticM α) : GrindTacticM α := do
+  if items.isEmpty then
+    k
+  else
+    let config := (← read).ctx.config
+    let config ← elabConfigItems config items
+    withReader (fun c => { c with ctx.config := config }) do k
+
 end Lean.Elab.Tactic.Grind

src/Lean/Elab/Tactic/Grind/Trace.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
+import Lean.Elab.Tactic.Grind.Config
 import Init.Grind.Interactive
 import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Tactic.Grind.Action
@@ -26,18 +27,20 @@ def mkFinish (maxIterations : Nat) : IO Action := do
 def maxIterations := 1000 -- **TODO**: Add option
 
 @[builtin_grind_tactic finishTrace] def evalFinishTrace : GrindTactic := fun stx => do
-  let a ← mkFinish maxIterations
-  let goal ← getMainGoal
-  withTracing do
-  match (← liftGrindM <| a.run goal) with
-  | .closed seq =>
-    replaceMainGoal []
-    let seq := Action.mkGrindSeq seq
-    Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax seq }
-  | .stuck gs =>
-    let goal :: _ := gs | throwError "`finish?` failed, but resulting goal is not available"
-    let params := (← read).params
-    let result ← liftGrindM do mkResult params (some goal)
-    throwError "`finish?` failed\n{← result.toMessageData}"
+  let `(grind| finish? $[$configItems]*) := stx | throwUnsupportedSyntax
+  withConfigItems configItems do
+    let a ← mkFinish maxIterations
+    let goal ← getMainGoal
+    withTracing do
+    match (← liftGrindM <| a.run goal) with
+    | .closed seq =>
+      replaceMainGoal []
+      let seq := Action.mkGrindSeq seq
+      Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax seq }
+    | .stuck gs =>
+      let goal :: _ := gs | throwError "`finish?` failed, but resulting goal is not available"
+      let params := (← read).params
+      let result ← liftGrindM do mkResult params (some goal)
+      throwError "`finish?` failed\n{← result.toMessageData}"
 
 end Lean.Elab.Tactic.Grind

tests/lean/run/grind_set_config.lean

@@ -20,3 +20,17 @@ example : f (x + 100) = a := by
     set_config (lia := true) in
     have : 3*x ≠ 1
     sorry
+
+opaque foo : Nat → Nat
+axiom fooAx1 : foo (x + 1) = foo x
+axiom fooAx2 : foo 0 ≥ 10
+
+example : foo 40 ≥ 5 := by
+  grind [fooAx1] =>
+    have := fooAx2
+    finish (gen := 50) (ematch := 50)
+
+example : foo 10 ≥ 5 := by
+  grind [fooAx1] =>
+    have := fooAx2
+    finish? (gen := 10) (ematch := 10)