feat: expose fields required for implementing linters outside of Lean core with detailed auto-fixes and diagnostic tags

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

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

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`.

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,17 +261,18 @@ 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 =>
                 logException (.error ref m!"linter {.ofConstName linter.name} failed: {msg}")
               | 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`.

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`.

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])

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)

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`. -/

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.

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