feat: hover information for grind anchors (#10779)

This PR implements hover information for `grind` anchors. Anchors are
stable hash codes for referencing terms in the grind state. The anchors
will be used when auto generating tactic scripts. The hover display the
following information:

1- In the `instantiate` tactic, it displays the type of the theorem
being instantiated.
<img width="952" height="125" alt="image"
src="https://github.com/user-attachments/assets/be949b87-cf9b-4f75-abe0-17751295de93"
/>

2- In the `cases` tactic, the hover information depends on the kind of
case-split.
  a) Proposition
<img width="1019" height="125" alt="image"
src="https://github.com/user-attachments/assets/253e2927-f18e-49ab-a8fc-2144657406d8"
/>

b) A hypotheses. In this case, you can opt to replace the anchor with
the hypothesis' name if it is accessible.
<img width="1019" height="178" alt="image"
src="https://github.com/user-attachments/assets/858b3751-4ef9-492d-a42f-c0743753a7de"
/>

c) A term. The hover displays just the type, by `grind` logs a silent
information with additional information
  
<img width="1376" height="148" alt="image"
src="https://github.com/user-attachments/assets/30078ca4-a886-49d9-912e-866f3567b0da"
/>

Author: leodemoura

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

@@ -104,6 +104,10 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
 @[builtin_grind_tactic ac] def evalAC : GrindTactic := fun _ => do
   evalCheck `ac AC.check AC.pp?
 
+def logTheoremAnchor (proof : Expr) : TermElabM Unit := do
+  let stx ← getRef
+  Term.addTermInfo' stx proof
+
 def ematchThms (thms : Array EMatchTheorem) : GrindTacticM Unit := do
   let progress ← liftGoalM <| if thms.isEmpty then ematch else ematchTheorems thms
   unless progress do
@@ -135,19 +139,24 @@ def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do
     ematchThms thms
   | _ => throwUnsupportedSyntax
 where
-  collectThms (numDigits : Nat) (anchorPrefix : UInt64) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindM Unit := do
+  collectThms (numDigits : Nat) (anchorPrefix : UInt64) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindTacticM Unit := do
+    let mut found : Std.HashSet Expr := {}
     for thm in thms do
       -- **Note**: `anchors` are cached using pointer addresses, if this is a performance issue, we should
       -- cache the theorem types.
       let type ← inferType thm.proof
-      let anchor ← getAnchor type
+      let anchor ← liftGrindM <| getAnchor type
       if isAnchorPrefix numDigits anchorPrefix anchor then
+        -- **Note**: We display the anchor term at most once.
+        unless found.contains type do
+          logTheoremAnchor thm.proof
+          found := found.insert type
         modify (·.push thm)
 
-  elabLocalEMatchTheorem (anchor : TSyntax `hexnum) : GrindTacticM (Array EMatchTheorem) := do
+  elabLocalEMatchTheorem (anchor : TSyntax `hexnum) : GrindTacticM (Array EMatchTheorem) := withRef anchor do
     let (numDigits, anchorPrefix) ← elabAnchor anchor
     let goal ← getMainGoal
-    let thms ← liftGrindM do StateT.run' (s := #[]) do
+    let thms ← StateT.run' (s := #[]) do
       collectThms numDigits anchorPrefix goal.ematch.thms
       collectThms numDigits anchorPrefix goal.ematch.newThms
       get
@@ -214,20 +223,47 @@ where
     | .cases _ | .intro | .inj | .ext | .symbol _ =>
       throwError "invalid modifier"
 
+def logAnchor (numDigits : Nat) (anchorPrefix : UInt64) (e : Expr) : TermElabM Unit := do
+  let stx ← getRef
+  if e.isFVar || e.isConst then
+    /-
+    **Note**: When `e` is a constant or free variable, the hover displays `e`
+    -/
+    Term.addTermInfo' stx e
+  else if (← isType e) then
+    /-
+    **Note**: If `e` is a type, we create a fake `sorry` to force `e` to be displayed
+    when we hover over the anchor.
+    We wrap the `sorry` with `id` to ensure the hover will not display `sorry : e`
+    -/
+    let e ← mkSorry e (synthetic := false)
+    let e ← mkId e
+    Term.addTermInfo' stx e
+  else
+    /-
+    **Note**: only the `e`s type is displayed when hovering over the anchor.
+    We add a silent info with the anchor declaration.
+    -/
+    Term.addTermInfo' stx e
+    logAt (severity := .information) (isSilent := true) stx
+       m!"#{anchorToString numDigits anchorPrefix} := {e}"
+
 @[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do
   match stx with
   | `(grind| cases #$anchor:hexnum) =>
     let (numDigits, val) ← elabAnchor anchor
     let goal ← getMainGoal
     let candidates := goal.split.candidates
-    let (goals, genNew) ← liftSearchM do
+    let (e, goals, genNew) ← liftSearchM do
       for c in candidates do
+        let e := c.getExpr
         let anchor ← getAnchor c.getExpr
         if isAnchorPrefix numDigits val anchor then
           let some result ← split? c
             | throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}"
-          return result
+          return (e, result)
       throwError "`cases` tactic failed, invalid anchor"
+    goal.withContext <| withRef anchor <| logAnchor numDigits val e
     let goals ← goals.filterMapM fun goal => do
       let (goal, _) ← liftGrindM <| SearchM.run goal do
         intros genNew

tests/lean/run/grind_interactive.lean

@@ -414,6 +414,11 @@ example : (∀ x, q x) → (∀ x, p x → p (f x)) → p x → p (f (f x)) := b
     show_thms
     instantiate #bfb8
 
+example : (∀ x, q x) → (∀ x, p x → p (f x)) → p x → p (f (f x)) := by
+  grind =>
+    show_thms
+    instantiate #bfb8
+
 /-- error: no local theorems -/
 #guard_msgs in
 example : (∀ x, q x) → (∀ x, p x → p (f x)) → p x → p (f (f x)) := by