From 0ad15fe98273448cff34de5b777550a82e09f5f9 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 8 Jan 2026 16:25:36 +1100
Subject: [PATCH] refactor: add message log capture helpers for tactic
 evaluation (#11933)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds utility functions for managing the message log during
tactic
evaluation, and refactors existing code to use them.

**New helpers in `Lean.Elab.Tactic`:**
- `withSuppressedMessages`: executes an action while suppressing new
messages
- `withCapturedMessages`: executes an action and returns any new
messages
- `hasErrorMessages`: checks if a message list contains errors

**Refactored to use these helpers:**
- `LibrarySearch.tryDischarger`: now uses `withSuppressedMessages`
- `Try.evalAndSuggest`: now uses `withSuppressedMessages`
- `Try.evalAndSuggestWithBy`: now uses `withSuppressedMessages`

These helpers provide a standard pattern for tactic validation that
needs to
inspect error messages (e.g., filtering out suggestions that produce
errors).

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
---
 src/Lean/Elab/Tactic/Basic.lean         | 27 +++++++++++++++++++++++++
 src/Lean/Elab/Tactic/Try.lean           | 26 +++++++++++-------------
 src/Lean/Meta/Tactic/LibrarySearch.lean |  5 ++---
 3 files changed, 41 insertions(+), 17 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 21a046ca8a..8afa8a0023 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -369,6 +369,33 @@ def withoutRecover (x : TacticM α) : TacticM α :=
 def withRecover (recover : Bool) (x : TacticM α) : TacticM α :=
   withReader (fun ctx => { ctx with recover }) x
 
+/-! ## Message log utilities -/
+
+/-- Execute an action while suppressing any new messages it generates.
+    Restores the original message log after the action completes.
+    Useful for trying tactics without polluting the message log with errors from failed attempts. -/
+def withSuppressedMessages (action : TacticM α) : TacticM α := do
+  let initialLog ← Core.getMessageLog
+  try
+    action
+  finally
+    Core.setMessageLog initialLog
+
+/-- Execute an action and return any new messages it generates.
+    Restores the original message log afterward.
+    Useful for inspecting messages produced by a tactic without committing them. -/
+def withCapturedMessages (action : TacticM α) : TacticM (α × List Message) := do
+  let initialLog ← Core.getMessageLog
+  let initialMsgCount := initialLog.toList.length
+  let result ← action
+  let newMsgs := (← Core.getMessageLog).toList.drop initialMsgCount
+  Core.setMessageLog initialLog
+  return (result, newMsgs)
+
+/-- Check if any messages in the list are errors. -/
+def hasErrorMessages (msgs : List Message) : Bool :=
+  msgs.any (·.severity == .error)
+
 /--
 Like `throwErrorAt`, but, if recovery is enabled, logs the error instead.
 -/
diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index 950b81577a..4956495358 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -821,13 +821,12 @@ private def addSuggestions (tk : Syntax) (s : Array Tactic.TryThis.Suggestion) :
     Tactic.TryThis.addSuggestions tk (s.map fun stx => stx) (origSpan? := (← getRef))
 
 def evalAndSuggest (tk : Syntax) (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) (config : Try.Config := {}) : TacticM Unit := do
-  let initialLog ← Core.getMessageLog
-  let tac' ← try
-    evalSuggest tac |>.run { terminal := true, root := tac, config, originalMaxHeartbeats }
-  catch _ =>
-    throwEvalAndSuggestFailed config
-  -- Restore message log to suppress "Try this" messages from intermediate tactic executions
-  Core.setMessageLog initialLog
+  -- Suppress "Try this" messages from intermediate tactic executions
+  let tac' ← withSuppressedMessages do
+    try
+      evalSuggest tac |>.run { terminal := true, root := tac, config, originalMaxHeartbeats }
+    catch _ =>
+      throwEvalAndSuggestFailed config
   let s := (getSuggestions tac')[*...config.max].toArray
   if s.isEmpty then
     throwEvalAndSuggestFailed config
@@ -985,13 +984,12 @@ private def wrapSuggestionWithBy (sugg : Tactic.TryThis.Suggestion) : TacticM Ta
 
 /-- Version of `evalAndSuggest` that wraps tactic suggestions with `by` for term mode. -/
 private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) (config : Try.Config) : TacticM Unit := do
-  let initialLog ← Core.getMessageLog
-  let tac' ← try
-    evalSuggest tac |>.run { terminal := true, root := tac, config, originalMaxHeartbeats }
-  catch _ =>
-    throwEvalAndSuggestFailed config
-  -- Restore message log to suppress "Try this" messages from intermediate tactic executions
-  Core.setMessageLog initialLog
+  -- Suppress "Try this" messages from intermediate tactic executions
+  let tac' ← withSuppressedMessages do
+    try
+      evalSuggest tac |>.run { terminal := true, root := tac, config, originalMaxHeartbeats }
+    catch _ =>
+      throwEvalAndSuggestFailed config
   let suggestions := (getSuggestions tac')[*...config.max].toArray
   if suggestions.isEmpty then
     throwEvalAndSuggestFailed config
diff --git a/src/Lean/Meta/Tactic/LibrarySearch.lean b/src/Lean/Meta/Tactic/LibrarySearch.lean
index 888cba27dd..05c4a0b5a8 100644
--- a/src/Lean/Meta/Tactic/LibrarySearch.lean
+++ b/src/Lean/Meta/Tactic/LibrarySearch.lean
@@ -84,9 +84,8 @@ def tryDischarger (mvarId : MVarId) : MetaM (Option (List MVarId)) := do
     let tacStx ← `(tactic| try?)
     let remainingGoals ← Elab.Term.TermElabM.run' <| Elab.Tactic.run subgoal do
       -- Suppress info messages from try?
-      let initialLog ← Core.getMessageLog
-      Elab.Tactic.evalTactic tacStx
-      Core.setMessageLog initialLog
+      Elab.Tactic.withSuppressedMessages do
+        Elab.Tactic.evalTactic tacStx
     if remainingGoals.isEmpty then
       return some []
     else