From e6b1f1984c27d26d2b9dd29fc7c24129a4ba99da Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 6 Nov 2025 17:31:04 +1100
Subject: [PATCH] feat: `suggestions` tactic generates hovers (#11098)

This PR updates the `suggestions` tactic so the printed message includes
hoverable type information (and displays scores and flags when
relevant).
---
 src/Lean/LibrarySuggestions/Basic.lean        | 11 ++++-
 tests/lean/run/grind_suggestions.lean         | 45 +++++++++++++++++++
 tests/lean/run/library_suggestions.lean       |  2 +-
 tests/lean/run/library_suggestions_local.lean |  7 ++-
 4 files changed, 61 insertions(+), 4 deletions(-)

diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
index f5eac90851..5bb3f3ce1e 100644
--- a/src/Lean/LibrarySuggestions/Basic.lean
+++ b/src/Lean/LibrarySuggestions/Basic.lean
@@ -417,7 +417,16 @@ open Lean.Elab.Tactic in
 @[builtin_tactic Lean.Parser.Tactic.suggestions] def evalSuggestions : Tactic := fun _ =>
   liftMetaTactic1 fun mvarId => do
     let suggestions ← select mvarId
-    logInfo m!"Library suggestions: {suggestions.map (·.name)}"
+    let mut msg : MessageData := "Library suggestions:"
+    -- Check if all scores are 1.0
+    let allScoresOne := suggestions.all (·.score == 1.0)
+    for s in suggestions do
+      msg := msg ++ Format.line ++ "  " ++ MessageData.ofConstName s.name
+      if !allScoresOne then
+        msg := msg ++ m!" (score: {s.score})"
+      if let some flag := s.flag then
+        msg := msg ++ m!" [{flag}]"
+    logInfo msg
     return mvarId
 
 end Lean.LibrarySuggestions
diff --git a/tests/lean/run/grind_suggestions.lean b/tests/lean/run/grind_suggestions.lean
index 36eb16bdde..8bd0c05c50 100644
--- a/tests/lean/run/grind_suggestions.lean
+++ b/tests/lean/run/grind_suggestions.lean
@@ -36,9 +36,54 @@ example : P 7 := by
 
 set_library_suggestions (fun _ _ => pure #[{ name := `p, score := 1.0 }])
 
+/--
+info: Library suggestions:
+  p
+-/
+#guard_msgs in
 example : P 7 := by
+  suggestions
   grind +suggestions
 
+set_library_suggestions (fun _ _ => pure #[{ name := `p, score := 0.5 }])
+
+/--
+info: Library suggestions:
+  p (score: 0.500000)
+-/
+#guard_msgs in
+example : P 7 := by
+  suggestions
+  grind +suggestions
+
+set_library_suggestions (fun _ _ => pure #[{ name := `p, score := 1.0, flag := some "←" }])
+
+/--
+info: Library suggestions:
+  p [←]
+---
+error: unexpected modifier ←
+-/
+#guard_msgs in
+example : P 7 := by
+  suggestions
+  grind +suggestions
+
+set_library_suggestions (fun _ _ => pure #[
+  { name := `p, score := 0.9 },
+  { name := `f, score := 0.7 }
+])
+
+/--
+info: Library suggestions:
+  p (score: 0.900000)
+  f (score: 0.700000)
+-/
+#guard_msgs in
+example : P 7 := by
+  suggestions
+  grind [p]
+
 set_library_suggestions (fun _ _ => pure #[{ name := `List.append_assoc, score := 1.0 }])
 
 -- Make sure there is no warning about the redundant theorem.
diff --git a/tests/lean/run/library_suggestions.lean b/tests/lean/run/library_suggestions.lean
index 71f64cab40..506bf87b8b 100644
--- a/tests/lean/run/library_suggestions.lean
+++ b/tests/lean/run/library_suggestions.lean
@@ -16,7 +16,7 @@ set_library_suggestions Nat
 
 set_library_suggestions (fun _ _ => pure #[])
 
-/-- info: Library suggestions: [] -/
+/-- info: Library suggestions: -/
 #guard_msgs in
 example : True := by
   suggestions
diff --git a/tests/lean/run/library_suggestions_local.lean b/tests/lean/run/library_suggestions_local.lean
index bbe6a6fe76..24aa295ba3 100644
--- a/tests/lean/run/library_suggestions_local.lean
+++ b/tests/lean/run/library_suggestions_local.lean
@@ -16,7 +16,8 @@ set_library_suggestions Lean.LibrarySuggestions.currentFile
 -- First test: should show only myLocalTheorem
 -- (not myLocalDef since it's a def, not Lean.shouldBeFiltered since it's in Lean namespace)
 /--
-info: Library suggestions: [myLocalTheorem]
+info: Library suggestions:
+  myLocalTheorem
 -/
 #guard_msgs in
 example : True := by
@@ -30,7 +31,9 @@ def myFunction (x : Nat) : Nat := x + 1
 
 -- Second test: should show only the two theorems (not myFunction)
 /--
-info: Library suggestions: [anotherTheorem, myLocalTheorem]
+info: Library suggestions:
+  anotherTheorem
+  myLocalTheorem
 -/
 #guard_msgs in
 example : False → True := by