feat: collect diagnostic explanations into hover popup

src/Lean/PrettyPrinter.lean

@@ -88,7 +88,8 @@ def ppSignature (c : Name) : MetaM FormatWithInfos := do
   if pp.raw.get (← getOptions) then
     return s!"{e} : {decl.type}"
   else
-    let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
+    let universes := pp.universes.get (← getOptions)
+    let (stx, infos) ← delabCore e (delab := delabConstWithSignature (universes := universes))
     return ⟨← ppTerm ⟨stx⟩, infos⟩  -- HACK: not a term
 
 private partial def noContext : MessageData → MessageData

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -26,6 +26,27 @@ open Snapshots
 
 open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
 
+/-- Structured hover content embedded in `Diagnostic.data?` by external tools (e.g. linters).
+Rendered as: **title** *(tag1, tag2)*\n\nbody -/
+private structure DiagnosticHoverData where
+  /-- Shown in bold as the hover heading. -/
+  hoverTitle : String := ""
+  /-- Shown dimmed in parentheses after the title. -/
+  hoverTags : Array String := #[]
+  /-- Markdown body with details. -/
+  hoverBody : String := ""
+  deriving FromJson
+
+private def DiagnosticHoverData.render (d : DiagnosticHoverData) : Option String :=
+  if d.hoverTitle.isEmpty && d.hoverBody.isEmpty then none
+  else
+    let title := if d.hoverTitle.isEmpty then "" else s!"**{d.hoverTitle}**"
+    let tags := if d.hoverTags.isEmpty then ""
+      else s!" *({", ".intercalate d.hoverTags.toList})*"
+    let header := title ++ tags
+    let parts := #[header, d.hoverBody].filter (!·.isEmpty)
+    some ("\n\n".intercalate parts.toList)
+
 def findCompletionCmdDataAtPos
     (doc : EditableDocument)
     (pos : String.Pos.Raw)
@@ -78,16 +99,25 @@ def handleHover (p : HoverParams)
     : RequestM (RequestTask (Option Hover)) := do
   let doc ← readDoc
   let text := doc.meta.text
-  let mkHover (s : String) (r : Lean.Syntax.Range) : Hover :=
+  let mkHover (s : String) (r : Option (Lsp.Range)) : Hover :=
     let s := Hover.rewriteExamples s
     {
       contents := {
         kind := MarkupKind.markdown
         value := s
       }
-      range? := r.toLspRange text
+      range? := r
     }
 
+  -- Extract hover link templates from initialization options
+  let linkTemplates : Array (String × String) :=
+    match (← read).initParams.initializationOptions? with
+    | some opts =>
+      match opts.hoverLinks? with
+      | some templates => templates.map fun t => (t.label, t.url)
+      | none => #[]
+    | none => #[]
+
   let hoverPos := text.lspPosToUtf8Pos p.position
   withWaitFindSnap doc (fun s => s.endPos > hoverPos)
     (notFoundX := pure none) fun snap => do
@@ -99,20 +129,35 @@ def handleHover (p : HoverParams)
           let docStr ← findDocString? snap.env kind
           return docStr.map (·, stx.getRange?.get!)
         | none => pure none
-      -- now try info tree
+      -- Collect all hover parts: info tree / parser docstring, then diagnostic hovers
+      let mut parts : Array String := #[]
+      let mut range? : Option Lsp.Range := none
+      -- info tree hover
       if let some result := snap.infoTree.hoverableInfoAtM? (m := Id) hoverPos then
         let ctx := result.ctx
         let info := result.info
-        if let some range := info.range? then
-          -- prefer info tree if at least as specific as parser docstring
-          if stxDoc?.all fun (_, stxRange) => stxRange.includes range then
-            if let some hoverFmt ← info.fmtHover? ctx then
-              return mkHover (toString hoverFmt.fmt) range
-
-      if let some (doc, range) := stxDoc? then
-        return mkHover doc range
-
-      return none
+        if let some r := info.range? then
+          if stxDoc?.all fun (_, stxRange) => stxRange.includes r then
+            if let some hoverFmt ← info.fmtHover? ctx linkTemplates then
+              parts := parts.push (toString hoverFmt.fmt)
+              range? := r.toLspRange text
+      -- parser docstring fallback
+      if parts.isEmpty then
+        if let some (d, r) := stxDoc? then
+          parts := parts.push d
+          range? := r.toLspRange text
+      -- diagnostic hovers from published diagnostics overlapping the cursor
+      let lspPos := p.position
+      let diags ← doc.collectCurrentDiagnostics
+      for diag in diags do
+        let r := diag.fullRange
+        if compare r.start lspPos != .gt && compare lspPos r.«end» != .gt then
+          if let some json := diag.data? then
+            if let some hoverData := (fromJson? json).toOption (α := DiagnosticHoverData) then
+              if let some rendered := hoverData.render then
+                parts := parts.push rendered
+      if parts.isEmpty then return none
+      return mkHover ("\n\n---\n\n".intercalate parts.toList) range?
 
 open Elab GoToKind in
 -- The `LeanLocationLink`s in this request get converted to `LocationLink` by the Watchdog process.

src/Lean/Server/InfoUtils.lean

@@ -355,31 +355,75 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
   return none
 
-/-- Construct a hover popup, if any, from an info node in a context.-/
-def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
+/-- Convert a module name to a source file path, e.g. `Init.Data.List.Basic` → `Init/Data/List/Basic.lean`. -/
+private def moduleToPath (mod : Name) : String :=
+  mod.toString (escape := false) |>.replace "." "/" |> (· ++ ".lean")
+
+/-- Convert a module name to a slash-separated path without extension, e.g. `Init.Data.List.Basic` → `Init/Data/List/Basic`. -/
+private def moduleToSlashPath (mod : Name) : String :=
+  mod.toString (escape := false) |>.replace "." "/"
+
+/-- Check whether a module belongs to Lean core (`Init`, `Lean`, or `Std`). -/
+private def isLeanCoreModule (mod : Name) : Bool :=
+  match mod.getRoot with
+  | `Init | `Lean | `Std => true
+  | _ => false
+
+/-- Substitute `{decl}`, `{module}`, `{path}`, `{line}` placeholders in a URL template. -/
+private def resolveHoverLink (template : String) (decl : Name) (mod : Name) (line : Nat) : String :=
+  template
+    |>.replace "{decl}" (toString decl)
+    |>.replace "{module}" (mod.toString (escape := false))
+    |>.replace "{path}" (moduleToPath mod)
+    |>.replace "{line}" (toString line)
+    |>.replace "{version}" Lean.versionStringCore
+    |>.replace "{githash}" Lean.githash
+
+/-- Construct a hover popup, if any, from an info node in a context.
+`linkTemplates` are `(label, urlTemplate)` pairs for generating hover links.
+An empty array means use built-in defaults for Lean core modules. -/
+def Info.fmtHover? (ci : ContextInfo) (i : Info)
+    (linkTemplates : Array (String × String) := #[]) : IO (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do
-    let mut fmts := #[]
+    let mut fmts : Array Format := #[]
     let mut infos := ∅
-    let modFmt ← try
-      let (termFmt, modFmt) ← fmtTermAndModule?
-      if let some f := termFmt then
-        fmts := fmts.push f.fmt
-        infos := f.infos
-      pure modFmt
-    catch _ => pure none
+    let (termFmt, modFmt) ← try fmtTermAndModule? catch _ => pure (none, none)
+    -- Build a single section: type signature, docstring, module path
+    if let some f := termFmt then
+      fmts := fmts.push f.fmt
+      infos := f.infos
     if let some m ← i.docString? then
       fmts := fmts.push m
     if let some f := modFmt then
       fmts := fmts.push f
     if fmts.isEmpty then
       return none
     else
-      return some ⟨f!"\n***\n".joinSep fmts.toList, infos⟩
+      return some ⟨f!"\n\n".joinSep fmts.toList, infos⟩
 
 where
   fmtModule? (decl : Name) : MetaM (Option Format) := do
     let some mod ← findModuleOf? decl | return none
-    return some f!"*import {mod}*"
+    let line ← do
+      if let some ranges ← findDeclarationRanges? decl then
+        pure ranges.range.pos.line
+      else
+        pure 1
+    let resolvedLinks : Array (String × String) :=
+      if linkTemplates.isEmpty then
+        if isLeanCoreModule mod then
+          #[("git", s!"https://github.com/leanprover/lean4/blob/v{Lean.versionStringCore}/src/{moduleToPath mod}#L{line}"),
+            ("ref", s!"https://lean-lang.org/doc/api/{moduleToSlashPath mod}.html#{decl}")]
+        else
+          #[]
+      else
+        linkTemplates.map fun (label, urlTmpl) =>
+          (label, resolveHoverLink urlTmpl decl mod line)
+    if resolvedLinks.isEmpty then
+      return some f!"*{mod}*"
+    else
+      let linkLines := resolvedLinks.toList.map fun (label, url) => s!"- **{label}**: {url}"
+      return some f!"*{mod}*\n{"\n".intercalate linkLines}"
 
   fmtTermAndModule? : MetaM (Option FormatWithInfos × Option Format) := do
     match i with
@@ -391,7 +435,8 @@ where
       let tp ← instantiateMVars (← Meta.inferType e)
       let tpFmt ← Meta.ppExpr tp
       if let .const c _ := e then
-        let eFmt ← PrettyPrinter.ppSignature c
+        let eFmt ← withOptions (fun o => pp.analyze.set (pp.universes.set o false) false) <|
+          PrettyPrinter.ppSignature c
         return (some { eFmt with fmt := f!"```lean\n{eFmt.fmt}\n```" }, ← fmtModule? c)
       let eFmt ← Meta.ppExpr e
       let lctx ← getLCtx