diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean index 07165ea994..05d97c47c9 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/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 /-- diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 6f48c27857..ff45659c65 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/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 diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 2f799ef879..8171fcc2c1 100644 --- a/src/Lean/Server/References.lean +++ b/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 diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index fb6f36446a..3b8a43c68e 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/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