From 350421604cad3012ce9c23fc984c235785c18f99 Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Sat, 28 Feb 2026 11:12:31 +0100 Subject: [PATCH 1/4] feat: extract DiagnosticTag and DiagnosticRelatedInformation modules Pulls these LSP types into their own prelude-friendly modules so downstream code (linters, widget bridges) can depend on them without importing the full Diagnostics module. --- .../Lsp/DiagnosticRelatedInformation.lean | 30 +++++++++++++ src/Lean/Data/Lsp/DiagnosticTag.lean | 42 +++++++++++++++++++ src/Lean/Data/Lsp/Diagnostics.lean | 28 +------------ 3 files changed, 74 insertions(+), 26 deletions(-) create mode 100644 src/Lean/Data/Lsp/DiagnosticRelatedInformation.lean create mode 100644 src/Lean/Data/Lsp/DiagnosticTag.lean diff --git a/src/Lean/Data/Lsp/DiagnosticRelatedInformation.lean b/src/Lean/Data/Lsp/DiagnosticRelatedInformation.lean new file mode 100644 index 000000000000..d08031092998 --- /dev/null +++ b/src/Lean/Data/Lsp/DiagnosticRelatedInformation.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2020 Marc Huisinga. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Marc Huisinga, Wojciech Nawrocki, Willem Vanhulle +-/ +module + +prelude +public import Lean.Data.Lsp.Basic + +public section + +/-! LSP diagnostic related information. + +Factored into its own module so that `Lean.Message` can use `DiagnosticRelatedInformation` +on `BaseMessage` without importing the full LSP diagnostics infrastructure. + +[LSP: DiagnosticRelatedInformation](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#diagnosticRelatedInformation) +-/ + +namespace Lean.Lsp + +/-- Represents a related message and source code location for a diagnostic. -/ +structure DiagnosticRelatedInformation where + location : Location + message : String + deriving Inhabited, BEq, ToJson, FromJson, Ord + +end Lean.Lsp diff --git a/src/Lean/Data/Lsp/DiagnosticTag.lean b/src/Lean/Data/Lsp/DiagnosticTag.lean new file mode 100644 index 000000000000..f44c3657014d --- /dev/null +++ b/src/Lean/Data/Lsp/DiagnosticTag.lean @@ -0,0 +1,42 @@ +/- +Copyright (c) 2020 Marc Huisinga. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Marc Huisinga, Wojciech Nawrocki, Willem Vanhulle +-/ +module + +prelude +public import Lean.Data.Json.FromToJson.Basic + +public section + +/-! LSP diagnostic tags. + +Factored into its own module so that `Lean.Message` can use `DiagnosticTag` +on `BaseMessage` without importing the full LSP diagnostics infrastructure. + +[LSP: DiagnosticTag](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#diagnosticTag) +-/ + +namespace Lean.Lsp + +/-- Tags representing additional metadata about the diagnostic. -/ +inductive DiagnosticTag where + /-- Unused or unnecessary code. Rendered as faded out eg for unused variables. -/ + | unnecessary + /-- Deprecated or obsolete code. Rendered with a strike-through. -/ + | deprecated + deriving Inhabited, BEq, Ord + +instance : FromJson DiagnosticTag := ⟨fun j => + match j.getNat? with + | Except.ok 1 => return DiagnosticTag.unnecessary + | Except.ok 2 => return DiagnosticTag.deprecated + | _ => throw "unknown DiagnosticTag"⟩ + +instance : ToJson DiagnosticTag := ⟨fun + | DiagnosticTag.unnecessary => (1 : Nat) + | DiagnosticTag.deprecated => (2 : Nat)⟩ + +end Lean.Lsp diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean index 9353793f7316..d0102efeec81 100644 --- a/src/Lean/Data/Lsp/Diagnostics.lean +++ b/src/Lean/Data/Lsp/Diagnostics.lean @@ -8,6 +8,8 @@ module prelude public import Lean.Data.Lsp.Basic +public import Lean.Data.Lsp.DiagnosticRelatedInformation +public import Lean.Data.Lsp.DiagnosticTag public import Lean.Data.Lsp.Utf16 @@ -58,24 +60,6 @@ instance : ToJson DiagnosticCode := ⟨fun | DiagnosticCode.int i => i | DiagnosticCode.string s => s⟩ -/-- Tags representing additional metadata about the diagnostic. -/ -inductive DiagnosticTag where - /-- Unused or unnecessary code. Rendered as faded out eg for unused variables. -/ - | unnecessary - /-- Deprecated or obsolete code. Rendered with a strike-through. -/ - | deprecated - deriving Inhabited, BEq, Ord - -instance : FromJson DiagnosticTag := ⟨fun j => - match j.getNat? with - | Except.ok 1 => return DiagnosticTag.unnecessary - | Except.ok 2 => return DiagnosticTag.deprecated - | _ => throw "unknown DiagnosticTag"⟩ - -instance : ToJson DiagnosticTag := ⟨fun - | DiagnosticTag.unnecessary => (1 : Nat) - | DiagnosticTag.deprecated => (2 : Nat)⟩ - /-- Custom diagnostic tags provided by the language server. We use a separate diagnostic field for this to avoid confusing LSP clients with our custom tags. @@ -105,14 +89,6 @@ instance : ToJson LeanDiagnosticTag where | .unsolvedGoals => (1 : Nat) | .goalsAccomplished => (2 : Nat) -/-- Represents a related message and source code location for a diagnostic. - This should be used to point to code locations that cause or are related to - a diagnostics, e.g when duplicating a symbol in a scope. -/ -structure DiagnosticRelatedInformation where - location : Location - message : String - deriving Inhabited, BEq, ToJson, FromJson, Ord - /-- Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource. LSP accepts a `Diagnostic := DiagnosticWith String`. From f430c4f60900fe7d64b6626993bd66aa4219c50c Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Sat, 28 Feb 2026 11:12:31 +0100 Subject: [PATCH 2/4] fix: preserve infoState across linter execution in Command.elabCommand --- src/Lean/Elab/Command.lean | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 85dd5021e27d..45d064de5f84 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -239,6 +239,18 @@ instance : MonadLog CommandElabM where let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data } modify fun s => { s with messages := s.messages.add msg } +private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : CommandElabM InfoTree := do + let ctx ← read + let s ← get + let scope := s.scopes.head! + let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees + let ctx := PartialContextInfo.commandCtx { + env := s.env, cmdEnv? := some s.env, fileMap := ctx.fileMap, mctx := {}, + currNamespace := scope.currNamespace, + openDecls := scope.openDecls, options := scope.opts, ngen := s.ngen + } + return InfoTree.context ctx tree + def runLinters (stx : Syntax) : CommandElabM Unit := do profileitM Exception "linting" (← getOptions) do withTraceNode `Elab.lint (fun _ => return m!"running linters") do @@ -249,7 +261,10 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do (tag := linter.name.toString) do let savedState ← get try - linter.run stx + -- Wrap linter execution with context preservation to ensure + -- any InfoTree nodes pushed by the linter are properly wrapped + withInfoTreeContext (mkInfoTree := mkInfoTree linter.name stx) do + linter.run stx catch ex => match ex with | Exception.error ref msg => @@ -257,9 +272,7 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do | Exception.internal _ _ => logException ex finally - -- TODO: it would be good to preserve even more state (#4363) but preserving info - -- trees currently breaks from linters adding context-less info nodes - modify fun s => { savedState with messages := s.messages, traceState := s.traceState } + modify fun s => { savedState with messages := s.messages, traceState := s.traceState, infoState := s.infoState } /-- Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function @@ -373,18 +386,6 @@ directly. unsafe builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkElabAttribute CommandElab `builtin_command_elab `command_elab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" -private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : CommandElabM InfoTree := do - let ctx ← read - let s ← get - let scope := s.scopes.head! - let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees - let ctx := PartialContextInfo.commandCtx { - env := s.env, cmdEnv? := some s.env, fileMap := ctx.fileMap, mctx := {}, - currNamespace := scope.currNamespace, - openDecls := scope.openDecls, options := scope.opts, ngen := s.ngen - } - return InfoTree.context ctx tree - /-- Disables incremental command reuse *and* reporting for `act` if `cond` is true by setting `Context.snap?` to `none`. From 9bfc78680e741a91ef6221ac1d32d595032967a1 Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Sat, 28 Feb 2026 11:12:31 +0100 Subject: [PATCH 3/4] feat: add tags, data, and relatedInformation to Lean Message Adds the three diagnostic fields to Message and threads them through Log and the InteractiveDiagnostic widget bridge so the LSP layer can emit them. Also preserves infoState on linter messages so consumers can attach quick-fix code actions. --- src/Lean/Log.lean | 4 +++- src/Lean/Message.lean | 8 ++++++++ src/Lean/Widget/InteractiveDiagnostic.lean | 12 +++++++----- 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean index 3d40ada008ff..018bc547afeb 100644 --- a/src/Lean/Log.lean +++ b/src/Lean/Log.lean @@ -108,7 +108,8 @@ If `getRef` has position information but `ref` does not, we use `getRef`. We use the `fileMap` to find the line and column numbers for the error message. -/ def logAt (ref : Syntax) (msgData : MessageData) - (severity : MessageSeverity := MessageSeverity.error) (isSilent : Bool := false) : m Unit := + (severity : MessageSeverity := MessageSeverity.error) (isSilent : Bool := false) + (diagnosticTags : Array Lsp.DiagnosticTag := #[]) : m Unit := unless severity == .error && msgData.hasSyntheticSorry do let severity := if severity == .warning && warningAsError.get (← getOptions) then .error else severity let ref := replaceRef ref (← MonadLog.getRef) @@ -123,6 +124,7 @@ def logAt (ref : Syntax) (msgData : MessageData) data := msgData severity isSilent + diagnosticTags } /-- Log a new error message using the given message data. The position is provided by `ref`. -/ diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index c82e6a18bb9a..c2245c31482b 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -11,6 +11,8 @@ prelude public import Init.Data.Slice.Array public import Lean.Util.PPExt public import Lean.Util.Sorry +public import Lean.Data.Lsp.DiagnosticRelatedInformation +public import Lean.Data.Lsp.DiagnosticTag import Init.Data.String.Search import Init.Data.Format.Macro import Init.Data.Iterators.Consumers.Collect @@ -444,6 +446,12 @@ structure BaseMessage (α : Type u) where caption : String := "" /-- The content of the message. -/ data : α + /-- Optional JSON-encoded data for LSP `Diagnostic.data?`. -/ + diagnosticData? : Option String := none + /-- LSP diagnostic tags (e.g. unnecessary, deprecated). -/ + diagnosticTags : Array Lsp.DiagnosticTag := #[] + /-- Related diagnostic information (e.g. other locations relevant to this diagnostic). -/ + relatedInformation? : Option (Array Lsp.DiagnosticRelatedInformation) := none deriving Inhabited, ToJson, FromJson /-- A `Message` is a richly formatted piece of information emitted by Lean. diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index 5fc9e0b22a31..ade9ab033c68 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -244,10 +244,7 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool | .error => .error let isSilent? := if m.isSilent then some true else none let source? := some "Lean 4" - let tags? := - if m.data.isDeprecationWarning then some #[.deprecated] - else if m.data.isUnusedVariableWarning then some #[.unnecessary] - else none + let tags? := if m.diagnosticTags.isEmpty then none else some m.diagnosticTags let leanTags? := if m.data.hasTag (· == `Tactic.unsolvedGoals) then some #[.unsolvedGoals] else if m.data.hasTag (· == `goalsAccomplished) then some #[.goalsAccomplished] @@ -256,6 +253,11 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool | .ok msg => msg | .error ex => TaggedText.text s!"[error when printing message: {ex.toString}]" let code? := (errorNameOfKind? m.kind).map (.string ·.toString) - pure { range, fullRange? := some fullRange, severity?, source?, message, tags?, leanTags?, isSilent?, code? } + let data? := m.diagnosticData?.bind fun s => + match Lean.Json.parse s with + | .ok j => some j + | .error _ => none + let relatedInformation? := m.relatedInformation? + pure { range, fullRange? := some fullRange, severity?, source?, message, tags?, leanTags?, isSilent?, code?, data?, relatedInformation? } end Lean.Widget From b41cf5fc0df5e06ae69dbdd314185f25093e26d8 Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Sat, 28 Feb 2026 11:12:31 +0100 Subject: [PATCH 4/4] feat: emit diagnostic tags from in-tree linters Updates Lean's built-in deprecated and unused-variable linters to use the new diagnosticTags field so editors render strikethrough/grey appropriately. Demonstrates the consumer pattern downstream linters will follow. --- src/Lean/Linter/Basic.lean | 5 +++-- src/Lean/Linter/Deprecated.lean | 9 ++++----- src/Lean/Linter/UnusedVariables.lean | 6 +----- 3 files changed, 8 insertions(+), 12 deletions(-) diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean index 86df00e63a5c..09bec0c7d623 100644 --- a/src/Lean/Linter/Basic.lean +++ b/src/Lean/Linter/Basic.lean @@ -87,9 +87,10 @@ def getLinterValueClippy (opt : Lean.Option Bool) (o : LinterOptions) : Bool := o.get opt.name (getLinterClippy o opt.defValue) def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] - (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := + (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) + (diagnosticTags : Array Lsp.DiagnosticTag := #[]) : m Unit := let disable := .note m!"This linter can be disabled with `set_option {linterOption.name} false`" - logWarningAt stx (.tagged linterOption.name m!"{msg}{disable}") + logAt stx (.tagged linterOption.name m!"{msg}{disable}") .warning (diagnosticTags := diagnosticTags) /-- If `linterOption` is enabled, print a linter warning message at the position determined by `stx`. diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index b10ae06037d4..8ee17b91fbdf 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -55,9 +55,6 @@ def setDeprecated {m} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (e def isDeprecated (env : Environment) (declName : Name) : Bool := Option.isSome <| deprecatedAttr.getParam? env declName -def _root_.Lean.MessageData.isDeprecationWarning (msg : MessageData) : Bool := - msg.hasTag (· == ``deprecatedAttr) - def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name := do (← deprecatedAttr.getParam? env declName).newName? @@ -92,5 +89,7 @@ def checkDeprecated (declName : Name) : MetaM Unit := do msg := msg ++ .note m!"`{.ofConstName newName true}` is protected. References to this \ constant must include {pfxCompStr}its prefix `{newPfx}` even when inside its namespace." pure msg - logWarning <| .tagged ``deprecatedAttr <| - m!"`{.ofConstName declName true}` has been deprecated" ++ extraMsg + logAt (← MonadLog.getRef) + (.tagged ``deprecatedAttr <| + m!"`{.ofConstName declName true}` has been deprecated" ++ extraMsg) + .warning (diagnosticTags := #[.deprecated]) diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index abcd4c3f88cf..e5e6f710fadc 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -570,14 +570,10 @@ def unusedVariables : Linter where -- Sort the outputs by position for (declStx, userName) in unused.qsort (·.1.getPos?.get! < ·.1.getPos?.get!) do - logLint linter.unusedVariables declStx m!"unused variable `{userName}`" + logLint linter.unusedVariables declStx m!"unused variable `{userName}`" (diagnosticTags := #[.unnecessary]) builtin_initialize addLinter unusedVariables end UnusedVariables end Linter -/-- Returns true if this is a message produced by the unused variable linter. -This is used to give these messages an additional "faded" style in the editor. -/ -def MessageData.isUnusedVariableWarning (msg : MessageData) : Bool := - msg.hasTag (· == Linter.linter.unusedVariables.name)