From 581188c0a4e7f82ab85af7165d1b6e0c74b8cd57 Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Sat, 28 Feb 2026 11:37:39 +0100 Subject: [PATCH] feat: collect diagnostic explanations into hover popup Hover popups now include any explanations attached to diagnostics in the hovered range, formatted with section breaks merged across adjacent diagnostics for compact display. --- src/Lean/PrettyPrinter.lean | 3 +- .../Server/FileWorker/RequestHandling.lean | 71 +++++++++++++++---- src/Lean/Server/InfoUtils.lean | 71 +++++++++++++++---- 3 files changed, 118 insertions(+), 27 deletions(-) diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 9af9eb4ddad8..59e38c367d8a 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/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 diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index a51b43e1894f..d07cef88f0ad 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/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. diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 4c6726ee74ad..48091e39a794 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -355,18 +355,43 @@ 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 @@ -374,12 +399,31 @@ def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) : 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