From 0b655b8f4abc827c2b78ef58ab7aec9e2091d2af Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Sat, 7 Nov 2026 22:11:16 +0000 Subject: [PATCH] fix: `finish` reports the thresholds of its own configuration `mkResult` records the configuration of the `GrindM` context, which `finish`, `finish?` and `set_config` set from their configuration items, in place of the configuration of `Params`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01QPKmiUooPkkAEYh2giBqfH --- src/Lean/Meta/Tactic/Grind/Main.lean | 2 +- tests/elab/grind_finish_threshold_config.lean | 28 +++++++++++++++++++ 2 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 tests/elab/grind_finish_threshold_config.lean diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean index 9e58b5df8252..837c538aeff4 100644 --- a/src/Lean/Meta/Tactic/Grind/Main.lean +++ b/src/Lean/Meta/Tactic/Grind/Main.lean @@ -422,7 +422,7 @@ def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do logInfo msg let rings := (← Sym.Arith.getArithState).rings let numBranches := (← get).numBranches - return { identity := params.identity, failure?, issues, config := params.config, counters, simp, splitDiags, ematchDiags, rings, numBranches } + return { identity := params.identity, failure?, issues, config := (← getConfig), counters, simp, splitDiags, ematchDiags, rings, numBranches } def GrindM.runAtGoal (mvarId : MVarId) (params : Params) (k : Goal → GrindM α) (evalTactic? : Option EvalTactic := none) : MetaM α := do let go : GrindM α := withGTransparency do diff --git a/tests/elab/grind_finish_threshold_config.lean b/tests/elab/grind_finish_threshold_config.lean new file mode 100644 index 000000000000..96d3ed71e104 --- /dev/null +++ b/tests/elab/grind_finish_threshold_config.lean @@ -0,0 +1,28 @@ +/-! The failure message of `finish` names the thresholds of its own configuration items. -/ + +opaque f : Nat → Nat + +/-- warning: declaration uses `sorry` -/ +#guard_msgs in +@[grind =] theorem f_succ (n : Nat) : f (n + 1) = f n + 1 := sorry + +/-- +error: `finish` has failed after reaching the thresholds `(instances := 5)` and `(ematch := 5)`, use `+verbose` to obtain diagnostic information +-/ +#guard_msgs in +example (h : f 0 = 0) : f 30 = 31 := by + grind => finish (instances := 5) + +/-- +error: `grind` has failed after reaching the thresholds `(instances := 5)` and `(ematch := 5)`, use `+verbose` to obtain diagnostic information +-/ +#guard_msgs in +example (h : f 0 = 0) : f 30 = 31 := by + grind (instances := 5) + +/-- +error: `finish` has failed after reaching the thresholds `(instances := 5)` and `(ematch := 5)`, use `+verbose` to obtain diagnostic information +-/ +#guard_msgs in +example (h : f 0 = 0) : f 30 = 31 := by + grind => set_config (instances := 5) in finish