From bb3dd13f729b163343ac06365d892dadfcab9528 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 27 Oct 2025 22:25:01 -0400
Subject: [PATCH] feat: `set_config` for setting `grind` configuration options
 (#10990)

This PR adds the `set_config` tactic for setting `grind` configuration
options. It uses the same syntax used for setting configuration options
in the `grind` main tactic.
---
 src/Init/Grind/Interactive.lean               |  5 +++
 src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 32 ++++++-------------
 src/Lean/Elab/Tactic/Grind/Config.lean        | 16 ++++++++++
 tests/lean/run/grind_set_config.lean          |  9 +++++-
 4 files changed, 38 insertions(+), 24 deletions(-)

diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index a8e23143e5..48744ca52c 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -240,6 +240,11 @@ syntax (name := exposeNames) "expose_names" : grind
 but it sets the option only within the tactics `tacs`. -/
 syntax (name := setOption) "set_option " (ident (noWs "." noWs ident)?) ppSpace optionValue " in " grindSeq : grind
 
+/--
+`set_config configItem+ in tacs` executes `tacs` with the updated configuration options `configItem+`
+-/
+syntax (name := setConfig) "set_config " configItem+ " in " grindSeq : grind
+
 /--
 Proves `<term>` using the current `grind` state and default search strategy.
 -/
diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index 8dd3a41818..f0de852e42 100644
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -426,30 +426,16 @@ where
   liftGrindM <| resetAnchors
   replaceMainGoal [{ goal with mvarId }]
 
-def isGrindConfigField? (stx : Syntax) : CoreM (Option Name) := do
-  unless stx.isIdent do return none
-  let id := stx.getId
-  let env ← getEnv
-  let info := getStructureInfo env ``Grind.Config
-  unless info.fieldNames.contains id do return none
-  return some id
-
 @[builtin_grind_tactic setOption] def elabSetOption : GrindTactic := fun stx => do
-  if let some fieldName ← isGrindConfigField? stx[1] then
-    let val := stx[3]
-    let val ← match val.isNatLit? with
-      | some num => pure <| DataValue.ofNat num
-      | none     => match val with
-        | Syntax.atom _ "true"  => pure <| DataValue.ofBool true
-        | Syntax.atom _ "false" => pure <| DataValue.ofBool false
-        | _ => throwErrorAt val "`grind` configuration option must be a Boolean or a numeral"
-    let config := (← read).ctx.config
-    let config ← setConfigField config fieldName val
-    withReader (fun c => { c with ctx.config := config }) do
-      evalGrindTactic stx[5]
-  else
-    let options ← Elab.elabSetOption stx[1] stx[3]
-    withOptions (fun _ => options) do evalGrindTactic stx[5]
+  let options ← Elab.elabSetOption stx[1] stx[3]
+  withOptions (fun _ => options) do evalGrindTactic stx[5]
+
+@[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
 
 @[builtin_grind_tactic mbtc] def elabMBTC : GrindTactic := fun _ => do
   liftGoalM do
diff --git a/src/Lean/Elab/Tactic/Grind/Config.lean b/src/Lean/Elab/Tactic/Grind/Config.lean
index 6e6519e218..b90a38c3cc 100644
--- a/src/Lean/Elab/Tactic/Grind/Config.lean
+++ b/src/Lean/Elab/Tactic/Grind/Config.lean
@@ -13,4 +13,20 @@ namespace Lean.Elab.Tactic.Grind
 /-- Sets a field of the `grind` configuration object. -/
 declare_config_getter setConfigField Grind.Config
 
+def elabConfigItems (init : Grind.Config) (items : Array (TSyntax `Lean.Parser.Tactic.configItem))
+    : CoreM Grind.Config := do
+  let mut config := init
+  for item in items do
+    match item with
+    | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := true))
+    | `(Lean.Parser.Tactic.configItem| +$fieldName:ident) =>
+      config ← setConfigField config fieldName.getId true
+    | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := false))
+    | `(Lean.Parser.Tactic.configItem| -$fieldName:ident) =>
+      config ← setConfigField config fieldName.getId false
+    | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := $val:num)) =>
+      config ← setConfigField config fieldName.getId (.ofNat val.getNat)
+    | _ => throwErrorAt item "unexpected configuration option"
+  return config
+
 end Lean.Elab.Tactic.Grind
diff --git a/tests/lean/run/grind_set_config.lean b/tests/lean/run/grind_set_config.lean
index 8df3acc450..c857a959fb 100644
--- a/tests/lean/run/grind_set_config.lean
+++ b/tests/lean/run/grind_set_config.lean
@@ -5,11 +5,18 @@ theorem fax : f (x + 1) = g (f x) := sorry
 
 example : f (x + 100) = a := by
   grind =>
-    set_option gen 15 in
+    set_config (gen := 15) -cutsat in
     -- The following instantiations should not fail since we set
     -- `gen` to 15
     use [fax]; use [fax]; use [fax]; use [fax]; use [fax]
     use [fax]; use [fax]; use [fax]; use [fax]; use [fax]
     use [fax]; use [fax]; use [fax]; use [fax]; use [fax]
     fail_if_success use [fax] -- should fail
+    fail_if_success have : 2*x ≠ 1 -- cutsat is disabled
+    set_config +cutsat in
+    have : 2*x ≠ 1
+    set_config (cutsat := false) in
+    fail_if_success have : 3*x ≠ 1
+    set_config (cutsat := true) in
+    have : 3*x ≠ 1
     sorry