feat: FileWorker handling of --no-build

src/Lean/Data/Lsp/Extra.lean

@@ -18,7 +18,7 @@ structure LeanDidOpenTextDocumentParams extends DidOpenTextDocumentParams where
   /--
     Further flags passed to `lake print-paths` for the opened document.
     Used for forwarding `--no-build` on initial open. -/
-  extraPrintPathsFlags? : Option (Array String)
+  extraPrintPathsFlags? : Option (Array String) := none
   deriving FromJson, ToJson
 
 /-- `textDocument/waitForDiagnostics` client->server request.

src/Lean/Server/FileWorker.lean

@@ -159,7 +159,7 @@ section Initialization
   Compilation progress is reported to `hOut` via LSP notifications. Return the search path for
   source files. -/
   partial def lakeSetupSearchPath (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do
-    let args := #["print-paths"] ++ imports.map (toString ·.module)
+    let args := #["print-paths"] ++ imports.map (toString ·.module) ++ m.extraPrintPathsFlags
     let cmdStr := " ".intercalate (toString lakePath :: args.toList)
     let lakeProc ← Process.spawn {
       stdin  := Process.Stdio.null
@@ -336,7 +336,7 @@ section NotificationHandling
     let newVersion := docId.version?.getD 0
     if ¬ changes.isEmpty then
       let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText⟩
+      updateDocument ⟨docId.uri, newVersion, newDocText, oldDoc.meta.extraPrintPathsFlags⟩
 
   def handleCancelRequest (p : CancelParams) : WorkerM Unit := do
     updatePendingRequests (fun pendingRequests => pendingRequests.erase p.id)
@@ -476,14 +476,15 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
   let initParams ← i.readLspRequestAs "initialize" InitializeParams
-  let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
+  let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" LeanDidOpenTextDocumentParams
+  let extraPrintPathsFlags := param.extraPrintPathsFlags?.getD #[]
   let doc := param.textDocument
   /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
     "\n", which should be enough to handle both LF and CRLF correctly.
     This is because LSP always refers to characters by (line, column),
     so if we get the line number correct it shouldn't matter that there
     is a CR there. -/
-  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
+  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, extraPrintPathsFlags⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try

src/Lean/Server/Utils.lean

@@ -65,9 +65,10 @@ end IO
 namespace Lean.Server
 
 structure DocumentMeta where
-  uri     : Lsp.DocumentUri
-  version : Nat
-  text    : FileMap
+  uri                  : Lsp.DocumentUri
+  version              : Nat
+  text                 : FileMap
+  extraPrintPathsFlags : Array String
   deriving Inhabited
 
 def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where

src/Lean/Server/Watchdog.lean

@@ -237,7 +237,7 @@ section ServerM
       | Except.ok ev   => ev
       | Except.error e => WorkerEvent.ioError e
 
-  def startFileWorker (m : DocumentMeta) (extraPrintPathsFlags : Array String := #[]) : ServerM Unit := do
+  def startFileWorker (m : DocumentMeta) : ServerM Unit := do
     publishProgressAtPos m 0 (← read).hOut
     let st ← read
     let workerProc ← Process.spawn {
@@ -268,7 +268,7 @@ section ServerM
           version    := m.version
           text       := m.text.source
         }
-        extraPrintPathsFlags? := extraPrintPathsFlags
+        extraPrintPathsFlags? := m.extraPrintPathsFlags
         : LeanDidOpenTextDocumentParams
       }
     }
@@ -388,7 +388,7 @@ section NotificationHandling
        This is because LSP always refers to characters by (line, column),
        so if we get the line number correct it shouldn't matter that there
        is a CR there. -/
-    startFileWorker ⟨doc.uri, doc.version, doc.text.toFileMap⟩ (p.extraPrintPathsFlags?.getD #[])
+    startFileWorker ⟨doc.uri, doc.version, doc.text.toFileMap, p.extraPrintPathsFlags?.getD #[]⟩
 
   def handleDidChange (p : DidChangeTextDocumentParams) : ServerM Unit := do
     let doc := p.textDocument
@@ -399,7 +399,7 @@ section NotificationHandling
     if changes.isEmpty then
       return
     let newDocText := foldDocumentChanges changes oldDoc.text
-    let newDoc : DocumentMeta := ⟨doc.uri, newVersion, newDocText⟩
+    let newDoc : DocumentMeta := ⟨doc.uri, newVersion, newDocText, oldDoc.extraPrintPathsFlags⟩
     updateFileWorkers { fw with doc := newDoc }
     tryWriteMessage doc.uri (Notification.mk "textDocument/didChange" p) (restartCrashedWorker := true)