adapt says, hint and guard_msg outputs

Author: mhuisi

Mathlib.lean

@@ -4092,6 +4092,7 @@ import Mathlib.InformationTheory.KullbackLeibler.KLFun
 import Mathlib.Init
 import Mathlib.Lean.ContextInfo
 import Mathlib.Lean.CoreM
+import Mathlib.Lean.Elab.InfoTree
 import Mathlib.Lean.Elab.Tactic.Basic
 import Mathlib.Lean.Elab.Tactic.Meta
 import Mathlib.Lean.Elab.Term

Mathlib/Lean/Elab/InfoTree.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marc Huisinga
+-/
+import Lean.Server.InfoUtils
+import Lean.Meta.TryThis
+
+/-!
+# Additions to `Lean.Elab.InfoTree.Main`
+-/
+
+namespace Lean.Elab
+
+open Lean.Meta
+open Lean.Meta.Tactic.TryThis
+
+/--
+Collects all suggestions from all `TryThisInfo`s in `trees`.
+`trees` is visited in order and suggestions in each tree are collected in post-order.
+-/
+def collectTryThisSuggestions (trees : PersistentArray InfoTree) :
+    Array Suggestion :=
+  go.run #[] |>.2
+where
+  /-- Visits all trees. -/
+  go : StateM (Array Suggestion) Unit := do
+    for tree in trees do
+      tree.visitM' (postNode := visitNode)
+  /-- Visits a node in a tree. -/
+  visitNode (_ctx : ContextInfo) (i : Info) (_children : PersistentArray InfoTree) :
+      StateM (Array Suggestion) Unit := do
+    let .ofCustomInfo ci := i
+      | return
+    let some tti := ci.value.get? TryThisInfo
+      | return
+    modify (·.push tti.suggestion)

Mathlib/Tactic/Basic.lean

@@ -125,4 +125,31 @@ elab (name := clearAuxDecl) "clear_aux_decl" : tactic => withMainContext do
 
 attribute [pp_with_univ] ULift PUnit PEmpty
 
+/-- Result of `withResetServerInfo`. -/
+structure withResetServerInfo.Result (α : Type) where
+  /-- Return value of the executed tactic. -/
+  result? : Option α
+  /-- Messages produced by the executed tactic. -/
+  msgs    : MessageLog
+  /-- Info trees produced by the executed tactic, wrapped in `CommandContextInfo.save`. -/
+  trees   : PersistentArray InfoTree
+
+/--
+Runs a tactic, returning any new messages and info trees rather than adding them to the state.
+-/
+def withResetServerInfo {α : Type} (t : TacticM α) :
+    TacticM (withResetServerInfo.Result α) := do
+  let (savedMsgs, savedTrees) ← modifyGetThe Core.State fun st =>
+    ((st.messages, st.infoState.trees), { st with messages := {}, infoState.trees := {} })
+  Prod.snd <$> MonadFinally.tryFinally' t fun result? => do
+    let msgs  ← Core.getMessageLog
+    let ist   ← getInfoState
+    let trees ← ist.trees.mapM fun tree => do
+      let tree := tree.substitute ist.assignment
+      let ctx := .commandCtx <| ← CommandContextInfo.save
+      return InfoTree.context ctx tree
+    modifyThe Core.State fun st =>
+      { st with messages := savedMsgs, infoState.trees := savedTrees }
+    return { result?, msgs, trees }
+
 end Mathlib.Tactic

Mathlib/Tactic/Hint.lean

@@ -7,6 +7,8 @@ import Lean.Meta.Tactic.TryThis
 import Batteries.Linter.UnreachableTactic
 import Batteries.Control.Nondet.Basic
 import Mathlib.Init
+import Mathlib.Lean.Elab.InfoTree
+import Mathlib.Tactic.Basic
 
 /-!
 # The `hint` tactic.
@@ -64,28 +66,14 @@ elab (name := registerHintStx)
 initialize
   Batteries.Linter.UnreachableTactic.ignoreTacticKindsRef.modify fun s => s.insert ``registerHintStx
 
-/--
-Extracts the `MessageData` from the first clickable `Try This:` diff widget in the message.
-Preserves (only) contexts and tags.
--/
-private def getFirstTryThisFromMessage? : MessageData → Option MessageData
-  | .ofWidget w msg => if w.id == ``Meta.Hint.tryThisDiffWidget then msg else none
-  | .nest _ msg
-  | .group msg => getFirstTryThisFromMessage? msg
-  | .compose msg₁ msg₂ => getFirstTryThisFromMessage? msg₁ <|> getFirstTryThisFromMessage? msg₂
-  | .withContext ctx msg => (getFirstTryThisFromMessage? msg).map <| .withContext ctx
-  | .withNamingContext ctx msg => (getFirstTryThisFromMessage? msg).map <| .withNamingContext ctx
-  | .tagged tag msg => (getFirstTryThisFromMessage? msg).map <| .tagged tag
-  | .ofFormatWithInfos _ | .ofGoal _ | .trace .. | .ofLazy .. => none
-
 /--
 Construct a suggestion for a tactic.
 * Check the passed `MessageLog` for an info message beginning with "Try this: ".
 * If found, use that as the suggestion.
 * Otherwise use the provided syntax.
 * Also, look for remaining goals and pretty print them after the suggestion.
 -/
-def suggestion (tac : TSyntax `tactic) (msgs : MessageLog := {}) : TacticM Suggestion := do
+def suggestion (tac : TSyntax `tactic) (trees : PersistentArray InfoTree) : TacticM Suggestion := do
   -- TODO `addExactSuggestion` has an option to construct `postInfo?`
   -- Factor that out so we can use it here instead of copying and pasting?
   let goals ← getGoals
@@ -102,27 +90,12 @@ def suggestion (tac : TSyntax `tactic) (msgs : MessageLog := {}) : TacticM Sugge
   -/
   -- let style? := if goals.isEmpty then some .success else none
   let preInfo? := if goals.isEmpty then some "🎉 " else none
-  let msg? : Option MessageData := msgs.toList.firstM (getFirstTryThisFromMessage? ·.data)
-  let suggestion ← match msg? with
-  | some m => pure <| SuggestionText.string (← m.toString)
-  | none => pure <| SuggestionText.tsyntax tac
+  let suggestions := collectTryThisSuggestions trees
+  let suggestion := match suggestions[0]? with
+  | some s => s.suggestion
+  | none => SuggestionText.tsyntax tac
   return { preInfo?, suggestion, postInfo? }
 
-/-- Run a tactic, returning any new messages rather than adding them to the message log. -/
-def withMessageLog (t : TacticM Unit) : TacticM MessageLog := do
-  let initMsgs ← modifyGetThe Core.State fun st => (st.messages, { st with messages := {} })
-  t
-  modifyGetThe Core.State fun st => (st.messages, { st with messages := initMsgs })
-
-/--
-Run a tactic, but revert any changes to info trees.
-We use this to inhibit the creation of widgets by subsidiary tactics.
--/
-def withoutInfoTrees (t : TacticM Unit) : TacticM Unit := do
-  let trees := (← getInfoState).trees
-  t
-  modifyInfoState fun s => { s with trees }
-
 /--
 Run all tactics registered using `register_hint`.
 Print a "Try these:" suggestion for each of the successful tactics.
@@ -136,11 +109,11 @@ def hint (stx : Syntax) : TacticM Unit := withMainContext do
   let tacs := (← getHints).toArray.qsort (·.1 > ·.1) |>.toList.map (·.2)
   let tacs := Nondet.ofList tacs
   let results := tacs.filterMapM fun t : TSyntax `tactic => do
-    if let some msgs ← observing? (withMessageLog (withoutInfoTrees (evalTactic t))) then
+    if let some { msgs, trees, .. } ← observing? (withResetServerInfo (evalTactic t)) then
       if msgs.hasErrors then
         return none
       else
-        return some (← getGoals, ← suggestion t msgs)
+        return some (← getGoals, ← suggestion t trees)
     else
       return none
   let results ← (results.toMLList.takeUpToFirst fun r => r.1.1.isEmpty).asArray

Mathlib/Tactic/Says.lean

@@ -7,6 +7,8 @@ import Mathlib.Init
 import Lean.Meta.Tactic.TryThis
 import Batteries.Linter.UnreachableTactic
 import Qq.Match
+import Mathlib.Lean.Elab.InfoTree
+import Mathlib.Tactic.Basic
 
 /-!
 # The `says` tactic combinator.
@@ -57,45 +59,30 @@ def parseAsTacticSeq (env : Environment) (input : String) (fileName := "<input>"
   else
     Except.error ((s.mkError "end of input").toErrorMsg ictx)
 
-/--
-Run `evalTactic`, capturing any new messages.
-The optional `only` argument allows selecting which messages should be captured,
-or left in the message log.
--/
-def evalTacticCapturingMessages (tac : TSyntax `tactic) (only : Message → Bool := fun _ => true) :
-    TacticM (List Message) := do
-  let mut msgs ← modifyGetThe Core.State fun st => (st.messages, { st with messages := {} })
-  try
-    evalTactic tac
-    let (capture, leave) := (← getThe Core.State).messages.toList.partition only
-    msgs := leave.foldl (·.add) msgs
-    return capture
-  catch e =>
-    msgs := msgs ++ (← getThe Core.State).messages
-    throw e
-  finally
-    modifyThe Core.State fun st => { st with messages := msgs }
-
-/--
-Run `evalTactic`, capturing any new info messages.
--/
-def evalTacticCapturingInfo (tac : TSyntax `tactic) : TacticM (List Message) :=
-  evalTacticCapturingMessages tac fun m => match m.severity with | .information => true | _ => false
-
 /--
 Run `evalTactic`, capturing a "Try this:" message and converting it back to syntax.
 -/
 def evalTacticCapturingTryThis (tac : TSyntax `tactic) : TacticM (TSyntax ``tacticSeq) := do
-  let msg ← match ← evalTacticCapturingInfo tac with
-  | [] => throwError m!"Tactic `{tac}` did not produce any messages."
-  | [msg] => msg.toString
-  | _ => throwError m!"Tactic `{tac}` produced multiple messages."
-  let tryThis ← match msg.dropPrefix? "Try this:" with
-  | none => throwError m!"Tactic output did not begin with 'Try this:': {msg}"
-  | some S => pure S.toString.removeLeadingSpaces
-  match parseAsTacticSeq (← getEnv) tryThis.trim with
-  | .ok stx => return stx
-  | .error err => throwError m!"Failed to parse tactic output: {tryThis}\n{err}"
+  let { trees, ..} ← withResetServerInfo <| evalTactic tac
+  let suggestions := collectTryThisSuggestions trees
+  let some s := suggestions[0]?
+    | throwError m!"Tactic `{tac}` did not produce a 'Try this:' suggestion."
+  let suggestion ← do
+    if let some msg := s.messageData? then
+      pure <| SuggestionText.string <| ← msg.toString
+    else
+      pure <| s.suggestion
+  match suggestion with
+  | .tsyntax (kind := ``tacticSeq) stx =>
+    return stx
+  | .tsyntax (kind := `tactic) stx =>
+    return ← `(tacticSeq| $stx:tactic)
+  | .tsyntax stx =>
+    throwError m!"Tactic `{tac}` produced a 'Try this:' suggestion with a non-tactic syntax: {stx}"
+  | .string s =>
+    match parseAsTacticSeq (← getEnv) s with
+    | .ok stx => return stx
+    | .error err => throwError m!"Failed to parse 'Try this:' suggestion: {s}\n{err}"
 
 /--
 If you write `X says`, where `X` is a tactic that produces a "Try this: Y" message,

MathlibTest/CalcQuestionMark.lean

@@ -9,8 +9,8 @@ When used from the widget that appears in VSCode, they insert correctly-indented
 
 /--
 info: Create calc tactic:
-  • calc
-        1 = 1 := by sorry
+  [apply] calc
+    1 = 1 := by sorry
 ---
 warning: declaration uses 'sorry'
 -/
@@ -22,8 +22,8 @@ example : 1 = 1 := by
 
 /--
 info: Create calc tactic:
-  • calc
-        a ≤ a := by sorry
+  [apply] calc
+    a ≤ a := by sorry
 ---
 warning: declaration uses 'sorry'
 -/
@@ -35,8 +35,8 @@ example (a : Nat) : a ≤ a := by
 
 /--
 info: Create calc tactic:
-  • calc
-          a ≤ a := by sorry
+  [apply] calc
+    a ≤ a := by sorry
 ---
 warning: declaration uses 'sorry'
 -/
@@ -48,18 +48,13 @@ example (a : Nat) : a ≤ a := by
 -- a deliberately long line
 /--
 info: Create calc tactic:
-  • calc
-        1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
-                            1 +
-                          1 +
-                        1 +
-                      1 +
-                    1 +
-                  1 +
-                1 +
-              1 =
-            8 + 8 + 8 + 8 :=
-          by sorry
+  [apply] calc
+    1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
+              1 +
+            1 +
+          1 =
+        8 + 8 + 8 + 8 :=
+      by sorry
 ---
 warning: declaration uses 'sorry'
 -/

MathlibTest/Change.lean

@@ -6,13 +6,13 @@ set_option autoImplicit true
 
 /--
 info: Try this:
-  change 0 = 1
+  [apply] change 0 = 1
 ---
 info: Try this:
-  change (fun x ↦ x) 0 = 1
+  [apply] change (fun x ↦ x) 0 = 1
 ---
 info: Try this:
-  change (fun x ↦ x) 0 = 1
+  [apply] change (fun x ↦ x) 0 = 1
 ---
 error: The term
   1 = 0

MathlibTest/DeprecateTo.lean

@@ -7,7 +7,7 @@ info: * Pairings:
 
 Try this:
 
-  /-- I also have a doc-string -/
+  [apply] /-- I also have a doc-string -/
   @[to_additive /-- With its additive doc-string -/
       ]
   theorem new_name_mul : True :=