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

@@ -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

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.

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

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