refactor: eliminate $/lean/ileanHeaderInfo (#12107)

src/Lean/Data/Lsp/Internal.lean

@@ -293,26 +293,18 @@ instance : FromJson ModuleRefs where
     node.foldlM (init := ∅) fun m k v =>
       return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
 
-/--
-Used in the `$/lean/ileanHeaderInfo` watchdog <- worker notifications.
-Contains the direct imports of the file managed by a worker.
--/
-structure LeanILeanHeaderInfoParams where
-  /-- Version of the file these imports are from. -/
-  version       : Nat
-  /-- Direct imports of this file. -/
-  directImports : Array ImportInfo
-  deriving FromJson, ToJson
-
 /--
 Used in the `$/lean/ileanHeaderSetupInfo` watchdog <- worker notifications.
-Contains status information about `lake setup-file`.
+Contains status information about `lake setup-file` and the direct imports of the file managed by
+a worker.
 -/
 structure LeanILeanHeaderSetupInfoParams where
   /-- Version of the file these imports are from. -/
   version        : Nat
   /-- Whether setting up the header using `lake setup-file` has failed. -/
   isSetupFailure : Bool
+  /-- Direct imports of this file. -/
+  directImports : Array ImportInfo
   deriving FromJson, ToJson
 
 /--

src/Lean/Server/FileWorker.lean

@@ -155,13 +155,12 @@ section Elab
     let param := { version := m.version, references, decls }
     return { method, param }
 
-  private def mkIleanHeaderInfoNotification (m : DocumentMeta)
-      (directImports : Array ImportInfo) : JsonRpc.Notification Lsp.LeanILeanHeaderInfoParams :=
-    { method := "$/lean/ileanHeaderInfo", param := { version := m.version, directImports } }
-
   private def mkIleanHeaderSetupInfoNotification (m : DocumentMeta)
-      (isSetupFailure : Bool) : JsonRpc.Notification Lsp.LeanILeanHeaderSetupInfoParams :=
-    { method := "$/lean/ileanHeaderSetupInfo", param := { version := m.version, isSetupFailure } }
+      (directImports : Array ImportInfo) (isSetupFailure : Bool) :
+      JsonRpc.Notification Lsp.LeanILeanHeaderSetupInfoParams := {
+    method := "$/lean/ileanHeaderSetupInfo"
+    param := { version := m.version, directImports, isSetupFailure }
+  }
 
   private def mkIleanInfoUpdateNotification : DocumentMeta → Array Elab.InfoTree →
       BaseIO (JsonRpc.Notification Lsp.LeanIleanInfoParams) :=
@@ -400,7 +399,6 @@ def setupImports
     return .error { diagnostics := .empty, result? := none, metaSnap := default }
 
   let header := stx.toModuleHeader
-  chanOut.sync.send <| .ofMsg <| mkIleanHeaderInfoNotification doc <| collectImports stx
   let fileSetupResult ← setupFile doc header fun stderrLine => do
     let progressDiagnostic := {
       range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
@@ -412,7 +410,8 @@ def setupImports
     chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[progressDiagnostic]
   let isSetupError := fileSetupResult matches .importsOutOfDate
     || fileSetupResult matches .error ..
-  chanOut.sync.send <| .ofMsg <| mkIleanHeaderSetupInfoNotification doc isSetupError
+  chanOut.sync.send <| .ofMsg <|
+    mkIleanHeaderSetupInfoNotification doc (collectImports stx) isSetupError
   -- clear progress notifications in the end
   chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[]
   let setup ← do

src/Lean/Server/References.lean

@@ -571,31 +571,6 @@ def removeIlean (self : References) (path : System.FilePath) : References :=
   namesToRemove.foldl (init := self) fun self name _ =>
     { self with ileans := self.ileans.erase name }
 
-/--
-Replaces the direct imports of a worker for the module `name` in `self` with
-a new set of direct imports.
--/
-def updateWorkerImports
-    (self          : References)
-    (name          : Name)
-    (moduleUri     : DocumentUri)
-    (version       : Nat)
-    (directImports : Array ImportInfo)
-    : IO References := do
-  let directImports ← DirectImports.convertImportInfos directImports
-  let some workerRefs := self.workers[name]?
-    | return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure? := none, refs := ∅, decls := ∅} }
-  match compare version workerRefs.version with
-  | .lt => return self
-  | .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure? := none, refs := ∅, decls := ∅} }
-  | .eq =>
-    let isSetupFailure? := workerRefs.isSetupFailure?
-    let refs := workerRefs.refs
-    let decls := workerRefs.decls
-    return { self with
-      workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs, decls }
-    }
-
 /--
 Replaces the direct imports of a worker for the module `name` in `self` with
 a new set of direct imports.
@@ -605,12 +580,13 @@ def updateWorkerSetupInfo
     (name           : Name)
     (moduleUri      : DocumentUri)
     (version        : Nat)
+    (directImports  : Array ImportInfo)
     (isSetupFailure : Bool)
     : IO References := do
+  let directImports ← DirectImports.convertImportInfos directImports
   let isSetupFailure? := some isSetupFailure
   let some workerRefs := self.workers[name]?
-    | return { self with workers := self.workers.insert name { moduleUri, version, directImports := ∅, isSetupFailure?, refs := ∅, decls := ∅} }
-  let directImports := workerRefs.directImports
+    | return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs := ∅, decls := ∅} }
   match compare version workerRefs.version with
   | .lt => return self
   | .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs := ∅, decls := ∅} }
@@ -702,7 +678,8 @@ def allDirectImports (self : References) : AllDirectImportsMap := Id.run do
   for (name, ilean) in self.ileans do
     allDirectImports := allDirectImports.insert name (ilean.moduleUri, ilean.directImports)
   for (name, worker) in self.workers do
-    allDirectImports := allDirectImports.insert name (worker.moduleUri, worker.directImports)
+    if worker.hasRefs then
+      allDirectImports := allDirectImports.insert name (worker.moduleUri, worker.directImports)
   return allDirectImports
 
 /--
@@ -723,7 +700,8 @@ The current imports in a file worker take precedence over those in .ilean files.
 -/
 def getDirectImports? (self : References) (mod : Name) : Option DirectImports := do
   if let some worker := self.workers[mod]? then
-    return worker.directImports
+    if worker.hasRefs then
+      return worker.directImports
   if let some ilean := self.ileans[mod]? then
     return ilean.directImports
   none

src/Lean/Server/Watchdog.lean

@@ -498,15 +498,10 @@ section ServerM
     let r? ← eraseGetPendingRequest uri id
     return r?.isSome
 
-  def handleILeanHeaderInfo (fw : FileWorker) (params : LeanILeanHeaderInfoParams) : ServerM Unit := do
-    let module := fw.doc.mod
-    let uri := fw.doc.uri
-    modifyReferencesIO (·.updateWorkerImports module uri params.version params.directImports)
-
   def handleILeanHeaderSetupInfo (fw : FileWorker) (params : LeanILeanHeaderSetupInfoParams) : ServerM Unit := do
     let module := fw.doc.mod
     let uri := fw.doc.uri
-    modifyReferencesIO (·.updateWorkerSetupInfo module uri params.version params.isSetupFailure)
+    modifyReferencesIO (·.updateWorkerSetupInfo module uri params.version params.directImports params.isSetupFailure)
 
   def handleIleanInfoUpdate (fw : FileWorker) (params : LeanIleanInfoParams) : ServerM Unit := do
     let module := fw.doc.mod
@@ -824,9 +819,6 @@ section ServerM
               let globalID ← (← read).serverRequestData.modifyGet
                 (·.trackOutboundRequest fw.doc.uri id)
               writeMessage (Message.request globalID method params?)
-        | .notification "$/lean/ileanHeaderInfo" =>
-          if let .ok params := parseNotificationParams? LeanILeanHeaderInfoParams msg then
-            handleILeanHeaderInfo fw params
         | .notification "$/lean/ileanHeaderSetupInfo" =>
           if let .ok params := parseNotificationParams? LeanILeanHeaderSetupInfoParams msg then
             handleILeanHeaderSetupInfo fw params