From dc5eb40ca3176761e56cb7874c8a8efa7b18d1b5 Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Fri, 7 Mar 2025 14:50:56 +0100
Subject: [PATCH] feat: 'unsolved goals' & 'goals accomplished' diagnostics
 (#7366)

This PR adds server-side support for dedicated 'unsolved goals' and
'goals accomplished' diagnostics that will have special support in the
Lean 4 VS Code extension. The special 'unsolved goals' diagnostic is
adapted from the 'unsolved goals' error diagnostic, while the 'goals
accomplished' diagnostic is issued when a `theorem` or `Prop`-typed
`example` has no errors or `sorry`s. The Lean 4 VS Code extension
companion PR is at leanprover/vscode-lean4#585.

Specifically, this PR extends the diagnostics served by the language
server with the following fields:
- `leanTags`: Custom tags that denote the kind of diagnostic that is
being served. As opposed to the `code`, `leanTags` should never be
displayed in the UI. Examples introduced by this PR are a tag to
distinguish 'unsolved goals' errors from other diagnostics, as well as a
tag to distinguish the new 'goals accomplished' diagnostic from other
diagnostics.
- `isSilent`: Whether a diagnostic should not be displayed as a regular
diagnostic in the editor. In VS Code, this means that the diagnostic is
displayed in the InfoView under 'Messages', but that it will not be
displayed under 'All Messages' and that it will also not be displayed
with a squiggly line.

The `isSilent` field is also implemented for `Message` so that silent
diagnostics can be logged in the elaborator. All code paths except for
the language server that display diagnostics to users are adjusted to
filter `Message`s with `isSilent := true`.
---
 src/Lean/AddDecl.lean                         |  2 +-
 src/Lean/Data/Lsp/Capabilities.lean           | 17 +++++++
 src/Lean/Data/Lsp/Diagnostics.lean            | 48 +++++++++++++++++--
 src/Lean/Elab/GuardMsgs.lean                  |  2 +
 src/Lean/Elab/MutualDef.lean                  | 48 ++++++++++++++++++-
 src/Lean/Language/Basic.lean                  | 13 ++---
 src/Lean/Language/Util.lean                   |  3 +-
 src/Lean/Log.lean                             | 12 ++++-
 src/Lean/Message.lean                         |  6 +++
 src/Lean/Server/FileWorker.lean               |  5 +-
 src/Lean/Widget/InteractiveDiagnostic.lean    |  7 ++-
 src/lake/Lake/Build/Actions.lean              |  3 +-
 src/lake/Lake/Load/Lean/Elab.lean             |  2 +
 tests/lean/interactive/4880.lean.expected.out |  1 +
 .../interactive/haveInfo.lean.expected.out    |  4 ++
 .../incrementalCombinator.lean.expected.out   |  4 ++
 .../incrementalTactic.lean.expected.out       |  4 ++
 .../interactive/issue4527.lean.expected.out   |  1 +
 18 files changed, 162 insertions(+), 20 deletions(-)

diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index e965135791..d934bf6ffc 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -82,7 +82,7 @@ where doAdd := do
   profileitM Exception "type checking" (← getOptions) do
     withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
       if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning m!"declaration uses 'sorry'"
+        logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
       let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
         |> ofExceptKernelException
       setEnv env
diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean
index 8b6c6d12a9..4af49333af 100644
--- a/src/Lean/Data/Lsp/Capabilities.lean
+++ b/src/Lean/Data/Lsp/Capabilities.lean
@@ -59,12 +59,29 @@ structure WorkspaceClientCapabilities where
   workspaceEdit? : Option WorkspaceEditClientCapabilities := none
   deriving ToJson, FromJson
 
+structure LeanClientCapabilities where
+  /--
+  Whether the client supports `DiagnosticWith.isSilent = true`.
+  If `none` or `false`, silent diagnostics will not be served to the client.
+  -/
+  silentDiagnosticSupport? : Option Bool := none
+  deriving ToJson, FromJson
+
 structure ClientCapabilities where
   textDocument? : Option TextDocumentClientCapabilities := none
   window?       : Option WindowClientCapabilities       := none
   workspace?    : Option WorkspaceClientCapabilities    := none
+  /-- Capabilties for Lean language server extensions. -/
+  lean?         : Option LeanClientCapabilities         := none
   deriving ToJson, FromJson
 
+def ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool := Id.run do
+  let some lean := c.lean?
+    | return false
+  let some silentDiagnosticSupport := lean.silentDiagnosticSupport?
+    | return false
+  return silentDiagnosticSupport
+
 -- TODO largely unimplemented
 structure ServerCapabilities where
   textDocumentSync?         : Option TextDocumentSyncOptions := none
diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index da81c222a3..9dca235f30 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -66,13 +66,42 @@ inductive DiagnosticTag where
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
-  | Except.ok 1 => return DiagnosticTag.unnecessary
-  | Except.ok 2 => return DiagnosticTag.deprecated
-  | _      => throw "unknown DiagnosticTag"⟩
+  | 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)⟩
+  | 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.
+-/
+inductive LeanDiagnosticTag where
+  /--
+  Diagnostics representing an "unsolved goals" error.
+  Corresponds to `MessageData.tagged `Tactic.unsolvedGoals ..`.
+  -/
+  | unsolvedGoals
+  /--
+  Diagnostics representing a "goals accomplished" silent message.
+  Corresponds to `MessageData.tagged `goalsAccomplished ..`.
+  -/
+  | goalsAccomplished
+  deriving Inhabited, BEq, Ord
+
+instance : FromJson LeanDiagnosticTag where
+  fromJson? j :=
+    match j.getNat? with
+    | .ok 1 => return LeanDiagnosticTag.unsolvedGoals
+    | .ok 2 => return LeanDiagnosticTag.goalsAccomplished
+    | _     => throw "unknown LeanDiagnosticTag"
+
+instance : ToJson LeanDiagnosticTag where
+  toJson
+  | .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
@@ -94,6 +123,13 @@ structure DiagnosticWith (α : Type) where
   /-- Extension: preserve semantic range of errors when truncating them for display purposes. -/
   fullRange? : Option Range := some range
   severity? : Option DiagnosticSeverity := none
+  /--
+  Extension: whether this diagnostic should not be displayed as a regular diagnostic in the editor.
+  In VS Code, this means that the diagnostic does not have a squiggly and is not displayed in
+  the InfoView under 'All Messages', but it is still displayed under 'Messages'.
+  Defaults to `false`.
+  -/
+  isSilent? : Option Bool := none
   /-- The diagnostic's code, which might appear in the user interface. -/
   code? : Option DiagnosticCode := none
   /-- A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'. -/
@@ -104,6 +140,8 @@ structure DiagnosticWith (α : Type) where
   message : α
   /-- Additional metadata about the diagnostic. -/
   tags? : Option (Array DiagnosticTag) := none
+  /-- Additional Lean-specific metadata about the diagnostic. -/
+  leanTags? : Option (Array LeanDiagnosticTag) := none
   /-- An array of related diagnostic information, e.g. when symbol-names within a scope collide all definitions can be marked via this property. -/
   relatedInformation? : Option (Array DiagnosticRelatedInformation) := none
   /-- A data entry field that is preserved between a `textDocument/publishDiagnostics` notification and `textDocument/codeAction` request. -/
diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean
index a19bb73a1e..846a4e0cdf 100644
--- a/src/Lean/Elab/GuardMsgs.lean
+++ b/src/Lean/Elab/GuardMsgs.lean
@@ -152,6 +152,8 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
     let mut toCheck : MessageLog := .empty
     let mut toPassthrough : MessageLog := .empty
     for msg in msgs.toList do
+      if msg.isSilent then
+        continue
       match specFn msg with
       | .check       => toCheck := toCheck.add msg
       | .drop        => pure ()
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index f15157c6bc..9cca94947d 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1068,6 +1068,47 @@ where
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"
 
+/--
+Logs a snapshot task that waits for the entire snapshot tree in `defsParsedSnap` and then logs a
+`goalsAccomplished` silent message for theorems and `Prop`-typed examples if the entire mutual block
+is error-free and contains no syntactical `sorry`s.
+-/
+private def logGoalsAccomplishedSnapshotTask (views : Array DefView)
+    (defsParsedSnap : DefsParsedSnapshot) : TermElabM Unit := do
+  let snaps := #[SnapshotTask.finished none (toSnapshotTree defsParsedSnap)] ++
+    (← getThe Core.State).snapshotTasks
+  let tree := SnapshotTree.mk { diagnostics := .empty } snaps
+  let logGoalsAccomplishedAct ← Term.wrapAsyncAsSnapshot (cancelTk? := none) fun () => do
+    -- NOTE: `waitAll` below ensures `getAll` will not block here
+    let logs := tree.getAll.map (·.diagnostics.msgLog)
+    let hasErrorOrSorry := logs.any fun log =>
+      log.reportedPlusUnreported.any fun msg =>
+        msg.severity matches .error || msg.data.hasTag (· == `hasSorry)
+    if hasErrorOrSorry then
+      return
+    for d in defsParsedSnap.defs, view in views do
+      let logGoalsAccomplished :=
+        let msgData := .tagged `goalsAccomplished m!"Goals accomplished!"
+        logAt view.ref msgData (severity := .information) (isSilent := true)
+      match view.kind with
+      | .theorem =>
+        logGoalsAccomplished
+      | .example =>
+        let some processedSnap := d.headerProcessedSnap.get
+          | continue
+        if ! (← isProp processedSnap.view.type) then
+          continue
+        logGoalsAccomplished
+      | _ => continue
+  let logGoalsAccomplishedTask ← BaseIO.mapTask (t := ← tree.waitAll) fun _ =>
+    logGoalsAccomplishedAct
+  Core.logSnapshotTask {
+    stx? := none
+    -- Use first line of the mutual block to avoid covering the progress of the whole mutual block
+    reportingRange? := (← getRef).getPos?.map fun pos => ⟨pos, pos⟩
+    task := logGoalsAccomplishedTask
+  }
+
 end Term
 namespace Command
 
@@ -1110,11 +1151,14 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
       }
       reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
     views := views.push view
+  let defsParsedSnap := { defs, diagnostics := .empty : DefsParsedSnapshot }
   if let some snap := snap? then
     -- no non-fatal diagnostics at this point
-    snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
+    snap.new.resolve <| .ofTyped defsParsedSnap
   let sc ← getScope
-  runTermElabM fun vars => Term.elabMutualDef vars sc views
+  runTermElabM fun vars => do
+    Term.elabMutualDef vars sc views
+    Term.logGoalsAccomplishedSnapshotTask views defsParsedSnap
 
 builtin_initialize
   registerTraceClass `Elab.definition.mkClosure
diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean
index 40acaa916b..3876b24e05 100644
--- a/src/Lean/Language/Basic.lean
+++ b/src/Lean/Language/Basic.lean
@@ -287,12 +287,13 @@ def reportMessages (msgLog : MessageLog) (opts : Options)
         {msg with severity}
       else
         msg
-    if json then
-      let j ← msg.toJson
-      IO.println j.compress
-    else
-      let s ← msg.toString includeEndPos
-      IO.print s
+    unless msg.isSilent do
+      if json then
+        let j ← msg.toJson
+        IO.println j.compress
+      else
+        let s ← msg.toString includeEndPos
+        IO.print s
     return hasErrors || msg.severity matches .error
 
 /--
diff --git a/src/Lean/Language/Util.lean b/src/Lean/Language/Util.lean
index 24751c4cb0..e9a1875758 100644
--- a/src/Lean/Language/Util.lean
+++ b/src/Lean/Language/Util.lean
@@ -22,7 +22,8 @@ where go range? s := do
   let mut desc := f!"{s.element.desc}"
   if let some range := range? then
     desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} "
-  desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString))
+  let msgs ← s.element.diagnostics.msgLog.toList.mapM (·.toString)
+  desc := desc ++ .prefixJoin "\n• " msgs
   withTraceNode `Elab.snapshotTree (fun _ => pure desc) do
     s.children.toList.forM fun c => go c.reportingRange? c.get
     if let some t := s.element.infoTree? then
diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean
index 6485e15a1f..d3a09b3ad5 100644
--- a/src/Lean/Log.lean
+++ b/src/Lean/Log.lean
@@ -58,7 +58,8 @@ Log the message `msgData` at the position provided by `ref` with the given `seve
 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) : m Unit :=
+def logAt (ref : Syntax) (msgData : MessageData)
+    (severity : MessageSeverity := MessageSeverity.error) (isSilent : Bool := false) : 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)
@@ -66,7 +67,14 @@ def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity :=
     let endPos := ref.getTailPos?.getD pos
     let fileMap ← getFileMap
     let msgData ← addMessageContext msgData
-    logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
+    logMessage {
+      fileName := (← getFileName)
+      pos := fileMap.toPosition pos
+      endPos := fileMap.toPosition endPos
+      data := msgData
+      severity
+      isSilent
+    }
 
 /-- Log a new error message using the given message data. The position is provided by `ref`. -/
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index e7e6bf8025..9730764f15 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -347,6 +347,12 @@ structure BaseMessage (α : Type u) where
   /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/
   keepFullRange : Bool := false
   severity      : MessageSeverity := .error
+  /--
+  If `true`, filter this message from non-language server output.
+  In the language server, silent messages are served as silent diagnostics.
+  See also `DiagnosticWith.isSilent?`.
+  -/
+  isSilent      : Bool := false
   caption       : String          := ""
   /-- The content of the message. -/
   data          : α
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index fab55b498d..8486dcbe9d 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -268,7 +268,10 @@ This option can only be set on the command line, not in the lakefile or via `set
               return (← ref.get).bind (·.get? MemorizedInteractiveDiagnostics) then
             pure memorized.diags
           else
-            let diags ← node.element.diagnostics.msgLog.toArray.mapM
+            let mut msgs := node.element.diagnostics.msgLog.toArray
+            if ! ctx.initParams.capabilities.silentDiagnosticSupport then
+              msgs := msgs.filter (! ·.isSilent)
+            let diags ← msgs.mapM
               (Widget.msgToInteractiveDiagnostic doc.meta.text · ctx.clientHasWidgets)
             if let some cacheRef := node.element.diagnostics.interactiveDiagsRef? then
               cacheRef.set <| some <| .mk { diags : MemorizedInteractiveDiagnostics }
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 25d3d02801..c7fd6cbe28 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -234,14 +234,19 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool
     | .information => .information
     | .warning     => .warning
     | .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 leanTags? :=
+    if m.data.hasTag (· == `Tactic.unsolvedGoals) then some #[.unsolvedGoals]
+    else if m.data.hasTag (· == `goalsAccomplished) then some #[.goalsAccomplished]
+    else none
   let message := match (← msgToInteractive m.data hasWidgets |>.toBaseIO) with
     | .ok msg => msg
     | .error ex => TaggedText.text s!"[error when printing message: {ex.toString}]"
-  pure { range, fullRange? := some fullRange, severity?, source?, message, tags? }
+  pure { range, fullRange? := some fullRange, severity?, source?, message, tags?, leanTags?, isSilent? }
 
 end Lean.Widget
diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index 356ecae7af..c8159f8570 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -56,7 +56,8 @@ def compileLeanModule
       if let .ok (msg : SerialMessage) := Json.parse ln >>= fromJson? then
         unless txt.isEmpty do
           logInfo s!"stdout:\n{txt}"
-        logSerialMessage msg
+        unless msg.isSilent do
+          logSerialMessage msg
         return txt
       else if txt.isEmpty && ln.isEmpty then
         return txt
diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean
index e05aa21b29..bc9cf3e00b 100644
--- a/src/lake/Lake/Load/Lean/Elab.lean
+++ b/src/lake/Lake/Load/Lean/Elab.lean
@@ -70,6 +70,8 @@ def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
 
   -- Log messages
   for msg in s.commandState.messages.toList do
+    if msg.isSilent then
+      continue
     match msg.severity with
     | MessageSeverity.information => logInfo (← msg.toString)
     | MessageSeverity.warning     => logWarning (← msg.toString)
diff --git a/tests/lean/interactive/4880.lean.expected.out b/tests/lean/interactive/4880.lean.expected.out
index c98090e749..5ebca885ae 100644
--- a/tests/lean/interactive/4880.lean.expected.out
+++ b/tests/lean/interactive/4880.lean.expected.out
@@ -47,6 +47,7 @@
    {"start": {"line": 34, "character": 13},
     "end": {"line": 35, "character": 0}},
    "message": "unsolved goals\n⊢ A",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 34, "character": 13},
     "end": {"line": 36, "character": 0}}}]}
diff --git a/tests/lean/interactive/haveInfo.lean.expected.out b/tests/lean/interactive/haveInfo.lean.expected.out
index 786f0ecea5..7cb553e8e4 100644
--- a/tests/lean/interactive/haveInfo.lean.expected.out
+++ b/tests/lean/interactive/haveInfo.lean.expected.out
@@ -6,6 +6,7 @@
    "range":
    {"start": {"line": 4, "character": 17}, "end": {"line": 5, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 4, "character": 17}, "end": {"line": 7, "character": 8}}},
   {"source": "Lean 4",
@@ -14,6 +15,7 @@
    {"start": {"line": 11, "character": 17},
     "end": {"line": 12, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 11, "character": 17},
     "end": {"line": 14, "character": 8}}},
@@ -23,6 +25,7 @@
    {"start": {"line": 18, "character": 17},
     "end": {"line": 19, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 18, "character": 17},
     "end": {"line": 21, "character": 8}}},
@@ -32,6 +35,7 @@
    {"start": {"line": 25, "character": 17},
     "end": {"line": 26, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 25, "character": 17},
     "end": {"line": 28, "character": 8}}}]}
diff --git a/tests/lean/interactive/incrementalCombinator.lean.expected.out b/tests/lean/interactive/incrementalCombinator.lean.expected.out
index 23e110d3d7..8a4f7f9bb1 100644
--- a/tests/lean/interactive/incrementalCombinator.lean.expected.out
+++ b/tests/lean/interactive/incrementalCombinator.lean.expected.out
@@ -33,6 +33,7 @@ sh
    "range":
    {"start": {"line": 2, "character": 17}, "end": {"line": 3, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 2, "character": 17},
     "end": {"line": 6, "character": 18}}},
@@ -41,6 +42,7 @@ sh
    "range":
    {"start": {"line": 1, "character": 24}, "end": {"line": 2, "character": 0}},
    "message": "unsolved goals\nthis : True\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 1, "character": 24},
     "end": {"line": 6, "character": 18}}}]}
@@ -53,6 +55,7 @@ sh
    "range":
    {"start": {"line": 2, "character": 18}, "end": {"line": 3, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 2, "character": 18},
     "end": {"line": 6, "character": 18}}},
@@ -61,6 +64,7 @@ sh
    "range":
    {"start": {"line": 1, "character": 24}, "end": {"line": 2, "character": 0}},
    "message": "unsolved goals\nthis : True\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 1, "character": 24},
     "end": {"line": 6, "character": 18}}}]}
diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out
index b429e40063..d80721785b 100644
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -23,6 +23,7 @@ t 2
    "range":
    {"start": {"line": 2, "character": 22}, "end": {"line": 3, "character": 0}},
    "message": "unsolved goals\nthis : Nat → Nat → True\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 2, "character": 22},
     "end": {"line": 10, "character": 11}}}]}
@@ -52,6 +53,7 @@ t 2
    "range":
    {"start": {"line": 3, "character": 9}, "end": {"line": 3, "character": 16}},
    "message": "unsolved goals\n⊢ Nat",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 3, "character": 9},
     "end": {"line": 3, "character": 16}}}]}
@@ -83,6 +85,7 @@ s
    "range":
    {"start": {"line": 3, "character": 12}, "end": {"line": 3, "character": 16}},
    "message": "unsolved goals\ncase zero\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 3, "character": 12},
     "end": {"line": 3, "character": 16}}}]}
@@ -94,6 +97,7 @@ s
    "range":
    {"start": {"line": 2, "character": 6}, "end": {"line": 2, "character": 10}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 2, "character": 6}, "end": {"line": 2, "character": 10}}},
   {"source": "Lean 4",
diff --git a/tests/lean/interactive/issue4527.lean.expected.out b/tests/lean/interactive/issue4527.lean.expected.out
index 0a542d8842..2a9be78d5e 100644
--- a/tests/lean/interactive/issue4527.lean.expected.out
+++ b/tests/lean/interactive/issue4527.lean.expected.out
@@ -6,5 +6,6 @@
    "range":
    {"start": {"line": 1, "character": 2}, "end": {"line": 2, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 1, "character": 2}, "end": {"line": 3, "character": 8}}}]}