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

@@ -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

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

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

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

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

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

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

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 :=

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          : α

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 }

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

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

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)

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

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

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

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",

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