feat: diagnostics for stale dependencies (#3247)

Sends a diagnostic informing the user to run Restart File when a file
dependency is saved.

Based on #3014 because this feature was easier to implement with the new
architecture.

ToDo:
- [x] Adjust vscode-lean4 to display a notification when this diagnostic
appears in a non-annoying way
(leanprover/vscode-lean4#393)
- [x] Use a file watcher to identify changes to files not tracked by VS
Code
- [x] Rebase onto master when #3014 is merged

src/Init/Data/Ord.lean

@@ -6,6 +6,7 @@ Authors: Dany Fabian, Sebastian Ullrich
 
 prelude
 import Init.Data.String
+import Init.Data.Array.Basic
 
 inductive Ordering where
   | lt | eq | gt
@@ -87,11 +88,24 @@ def isGE : Ordering → Bool
 
 end Ordering
 
+/--
+Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
+`x = y` corresponds to `Ordering.eq`.
+-/
 @[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
   if x < y then Ordering.lt
   else if x = y then Ordering.eq
   else Ordering.gt
 
+/--
+Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
+`x == y` corresponds to `Ordering.eq`.
+-/
+@[inline] def compareOfLessAndBEq {α} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering :=
+  if x < y then .lt
+  else if x == y then .eq
+  else .gt
+
 /--
 Compare `a` and `b` lexicographically by `cmp₁` and `cmp₂`. `a` and `b` are
 first compared by `cmp₁`. If this returns 'equal', `a` and `b` are compared
@@ -147,6 +161,13 @@ instance : Ord USize where
 instance : Ord Char where
   compare x y := compareOfLessAndEq x y
 
+instance [Ord α] : Ord (Option α) where
+  compare
+  | none,   none   => .eq
+  | none,   some _ => .lt
+  | some _, none   => .gt
+  | some x, some y => compare x y
+
 /-- The lexicographic order on pairs. -/
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare p1 p2 := match compare p1.1 p2.1 with
@@ -210,4 +231,13 @@ returns 'equal', by `ord₂`.
 protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
+/--
+Creates an order which compares elements of an `Array` in lexicographic order.
+-/
+protected def arrayOrd [a : Ord α] : Ord (Array α) where
+  compare x y :=
+    let _ : LT α := a.toLT
+    let _ : BEq α := a.toBEq
+    compareOfLessAndBEq x.toList y.toList
+
 end Ord

src/Lean/Data/Lsp/Basic.lean

@@ -52,7 +52,7 @@ instance : LE Range := leOfOrd
 structure Location where
   uri : DocumentUri
   range : Range
-  deriving Inhabited, BEq, ToJson, FromJson
+  deriving Inhabited, BEq, ToJson, FromJson, Ord
 
 structure LocationLink where
   originSelectionRange? : Option Range

src/Lean/Data/Lsp/Diagnostics.lean

@@ -25,7 +25,7 @@ open Json
 
 inductive DiagnosticSeverity where
   | error | warning | information | hint
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticSeverity := ⟨fun j =>
   match j.getNat? with
@@ -45,7 +45,7 @@ instance : ToJson DiagnosticSeverity := ⟨fun
 inductive DiagnosticCode where
   | int (i : Int)
   | string (s : String)
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticCode := ⟨fun
   | num (i : Int) => return DiagnosticCode.int i
@@ -62,7 +62,7 @@ inductive DiagnosticTag where
   | unnecessary
   /-- Deprecated or obsolete code. Rendered with a strike-through. -/
   | deprecated
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
@@ -80,7 +80,7 @@ instance : ToJson DiagnosticTag := ⟨fun
 structure DiagnosticRelatedInformation where
   location : Location
   message : String
-  deriving Inhabited, BEq, ToJson, FromJson
+  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.
 
@@ -113,6 +113,29 @@ structure DiagnosticWith (α : Type) where
 def DiagnosticWith.fullRange (d : DiagnosticWith α) : Range :=
   d.fullRange?.getD d.range
 
+local instance [Ord α] : Ord (Array α) := Ord.arrayOrd
+
+/-- Restriction of `DiagnosticWith` to properties that are displayed to users in the InfoView. -/
+private structure DiagnosticWith.UserVisible (α : Type) where
+  range               : Range
+  fullRange?          : Option Range
+  severity?           : Option DiagnosticSeverity
+  code?               : Option DiagnosticCode
+  source?             : Option String
+  message             : α
+  tags?               : Option (Array DiagnosticTag)
+  relatedInformation? : Option (Array DiagnosticRelatedInformation)
+  deriving Ord
+
+/-- Extracts user-visible properties from the given `DiagnosticWith`. -/
+private def DiagnosticWith.UserVisible.ofDiagnostic (d : DiagnosticWith α)
+    : DiagnosticWith.UserVisible α :=
+  { d with }
+
+/-- Compares `DiagnosticWith` instances modulo non-user-facing properties. -/
+def compareByUserVisible [Ord α] (a b : DiagnosticWith α) : Ordering :=
+  compare (DiagnosticWith.UserVisible.ofDiagnostic a) (DiagnosticWith.UserVisible.ofDiagnostic b)
+
 abbrev Diagnostic := DiagnosticWith String
 
 /-- Parameters for the [`textDocument/publishDiagnostics` notification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_publishDiagnostics). -/

src/Lean/Data/Lsp/Internal.lean

@@ -161,14 +161,33 @@ instance : FromJson ModuleRefs where
     node.foldM (init := HashMap.empty) fun m k v =>
       return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
 
-/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
-
-Contains the file's definitions and references. -/
+/--
+Used in the `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog <- worker notifications.
+Contains the definitions and references of the file managed by a worker.
+-/
 structure LeanIleanInfoParams where
   /-- Version of the file these references are from. -/
   version    : Nat
   /-- All references for the file. -/
   references : ModuleRefs
   deriving FromJson, ToJson
 
+/--
+Used in the `$/lean/importClosure` watchdog <- worker notification.
+Contains the full import closure of the file managed by a worker.
+-/
+structure LeanImportClosureParams where
+  /-- Full import closure of the file. -/
+  importClosure : Array DocumentUri
+  deriving FromJson, ToJson
+
+/--
+Used in the `$/lean/importClosure` watchdog -> worker notification.
+Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.
+-/
+structure LeanStaleDependencyParams where
+  /-- The dependency that is stale. -/
+  staleDependency : DocumentUri
+  deriving FromJson, ToJson
+
 end Lean.Lsp

src/Lean/Data/Lsp/TextSync.lean

@@ -38,7 +38,7 @@ structure DidOpenTextDocumentParams where
 
 structure TextDocumentChangeRegistrationOptions where
   documentSelector? : Option DocumentSelector := none
-  syncKind : TextDocumentSyncKind
+  syncKind          : TextDocumentSyncKind
   deriving FromJson
 
 inductive TextDocumentContentChangeEvent where
@@ -61,13 +61,18 @@ instance TextDocumentContentChangeEvent.hasToJson : ToJson TextDocumentContentCh
     | TextDocumentContentChangeEvent.fullChange text => [⟨"text", toJson text⟩]⟩
 
 structure DidChangeTextDocumentParams where
-  textDocument : VersionedTextDocumentIdentifier
+  textDocument   : VersionedTextDocumentIdentifier
   contentChanges : Array TextDocumentContentChangeEvent
   deriving ToJson, FromJson
 
+structure DidSaveTextDocumentParams where
+  textDocument : TextDocumentIdentifier
+  text?        : Option String
+  deriving ToJson, FromJson
+
 -- TODO: missing:
 -- WillSaveTextDocumentParams, TextDocumentSaveReason,
--- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams
+-- TextDocumentSaveRegistrationOptions
 
 structure SaveOptions where
   includeText : Bool
@@ -81,11 +86,11 @@ structure DidCloseTextDocumentParams where
 
 /-- NOTE: This is defined twice in the spec. The latter version has more fields. -/
 structure TextDocumentSyncOptions where
-  openClose : Bool
-  change : TextDocumentSyncKind
-  willSave : Bool
+  openClose         : Bool
+  change            : TextDocumentSyncKind
+  willSave          : Bool
   willSaveWaitUntil : Bool
-  save? : Option SaveOptions := none
+  save?             : Option SaveOptions
   deriving ToJson, FromJson
 
 end Lsp

src/Lean/Server/FileSource.lean

@@ -37,6 +37,9 @@ instance : FileSource DidOpenTextDocumentParams :=
 instance : FileSource DidChangeTextDocumentParams :=
   ⟨fun p => fileSource p.textDocument⟩
 
+instance : FileSource DidSaveTextDocumentParams :=
+  ⟨fun p => fileSource p.textDocument⟩
+
 instance : FileSource DidCloseTextDocumentParams :=
   ⟨fun p => fileSource p.textDocument⟩