diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 498b9fe6e1..2b1098a87a 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -46,6 +46,8 @@ open Lsp open IO open Snapshots open Lean.Parser.Command +open Std (RBMap RBMap.empty) +open JsonRpc section Utils private def logSnapContent (s : Snapshot) (text : FileMap) : IO Unit := @@ -88,36 +90,18 @@ section Utils deriving Inhabited end Utils -open IO -open Std (RBMap RBMap.empty) -open JsonRpc - -section ServerM - -- Pending requests are tracked so they can be cancelled - abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) (fun a b => Decidable.decide (a < b)) - - structure ServerContext where - hIn : FS.Stream - hOut : FS.Stream - hLog : FS.Stream - docRef : IO.Ref EditableDocument - pendingRequestsRef : IO.Ref PendingRequestMap - - abbrev ServerM := ReaderT ServerContext IO - - def updatePendingRequests (map : PendingRequestMap → PendingRequestMap) : ServerM Unit := do - (←read).pendingRequestsRef.modify map - - /-- Elaborates the next command after `parentSnap` and emits diagnostics. -/ - private def nextCmdSnap (m : DocumentMeta) (parentSnap : Snapshot) (cancelTk : CancelToken) : ExceptT ElabTaskError ServerM Snapshot := do +/- Asynchronous snapshot elaboration. -/ +section Elab + /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/ + private def nextCmdSnap (m : DocumentMeta) (parentSnap : Snapshot) (cancelTk : CancelToken) (hOut : FS.Stream) + : ExceptT ElabTaskError IO Snapshot := do cancelTk.check - let st ← read let maybeSnap ← compileNextCmd m.text.source parentSnap -- TODO(MH): check for interrupt with increased precision cancelTk.check let sendDiagnostics (msgLog : MessageLog) : IO Unit := do let diagnostics ← msgLog.msgs.mapM (msgToDiagnostic m.text) - st.hOut.writeLspNotification { + hOut.writeLspNotification { method := "textDocument/publishDiagnostics" param := { uri := m.uri @@ -148,12 +132,31 @@ section ServerM sendDiagnostics msgLog throw ElabTaskError.eof - /-- Elaborates all commands after `initSnap`, emitting the diagnostics. -/ - def unfoldCmdSnaps (m : DocumentMeta) (initSnap : Snapshot) (cancelTk : CancelToken) : ServerM (AsyncList ElabTaskError Snapshot) := do - AsyncList.unfoldAsync (nextCmdSnap m . cancelTk (←read)) initSnap + /-- Elaborates all commands after `initSnap`, emitting the diagnostics into `hOut`. -/ + def unfoldCmdSnaps (m : DocumentMeta) (initSnap : Snapshot) (cancelTk : CancelToken) (hOut : FS.Stream) + : IO (AsyncList ElabTaskError Snapshot) := do + AsyncList.unfoldAsync (nextCmdSnap m . cancelTk hOut) initSnap +end Elab - /-- Use `leanpkg print-paths` to compile dependencies on the fly and add them to LEAN_PATH. -/ - partial def leanpkgSetupSearchPath (leanpkgPath : String) (m : DocumentMeta) (imports : Array Import) : ServerM Unit := do +-- Pending requests are tracked so they can be cancelled +abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) (fun a b => Decidable.decide (a < b)) + +structure ServerContext where + hIn : FS.Stream + hOut : FS.Stream + hLog : FS.Stream + srcSearchPath : SearchPath + docRef : IO.Ref EditableDocument + pendingRequestsRef : IO.Ref PendingRequestMap + +abbrev ServerM := ReaderT ServerContext IO + +/- Worker initialization sequence. -/ +section Initialization + /-- Use `leanpkg print-paths` to compile dependencies on the fly and add them to `LEAN_PATH`. + Compilation progress is reported to `hOut` via LSP notifications. Return the search path for + source files. -/ + partial def leanpkgSetupSearchPath (leanpkgPath : String) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do let leanpkgProc ← Process.spawn { stdin := Process.Stdio.null stdout := Process.Stdio.piped @@ -161,7 +164,6 @@ section ServerM cmd := leanpkgPath args := #["print-paths"] ++ imports.map (toString ·.module) } - let hOut := (← read).hOut -- progress notification: report latest stderr line let rec processStderr (acc : String) : IO String := do let line ← leanpkgProc.stderr.getLine @@ -183,23 +185,30 @@ section ServerM let stderr ← IO.ofExcept stderr.get if (← leanpkgProc.wait) == 0 then match stdout.split (· == '\n') with - | [""] => pure () -- e.g. no leanpkg.toml - | [leanPath, leanSrcPath] => searchPathRef.set (← parseSearchPath leanPath (← getBuiltinSearchPath)) - | _ => throw <| IO.userError s!"unexpected output from `leanpkg src-paths`:\n{stdout}\nstderr:{stderr}" + | [""] => pure [] -- e.g. no leanpkg.toml + | [leanPath, leanSrcPath] => let sp ← getBuiltinSearchPath + let sp ← addSearchPathFromEnv sp + let sp ← parseSearchPath leanPath sp + searchPathRef.set sp + return parseSearchPath leanSrcPath + | _ => throw <| IO.userError s!"unexpected output from `leanpkg print-paths`:\n{stdout}\nstderr:\n{stderr}" else - throw <| IO.userError stderr + throw <| IO.userError s!"`leanpkg src-paths` failed:\n{stdout}\nstderr:\n{stderr}" - /-- Compiles the contents of a Lean file. -/ - def compileDocument (m : DocumentMeta) : ServerM Unit := do + def compileHeader (m : DocumentMeta) (hOut : FS.Stream) : IO (Snapshot × SearchPath) := do let opts := {} -- TODO let inputCtx := Parser.mkInputContext m.text.source "" let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx let leanpkgPath ← match ← IO.getEnv "LEAN_SYSROOT" with | some path => s!"{path}/bin/leanpkg{System.FilePath.exeSuffix}" | _ => s!"{← appDir}/leanpkg{System.FilePath.exeSuffix}" + let mut srcSearchPath := match (← IO.getEnv "LEAN_SRC_PATH") with + | some p => parseSearchPath p + | none => [] -- NOTE: leanpkg does not exist in stage 0 (yet?) if (← fileExists leanpkgPath) then - leanpkgSetupSearchPath leanpkgPath m (Lean.Elab.headerToImports headerStx).toArray + let pkgSearchPath ← leanpkgSetupSearchPath leanpkgPath m (Lean.Elab.headerToImports headerStx).toArray hOut + srcSearchPath := srcSearchPath ++ pkgSearchPath let (headerEnv, msgLog) ← Elab.processHeader headerStx opts msgLog inputCtx let cmdState := Elab.Command.mkState headerEnv msgLog opts let opts := opts.setBool `interpreter.prefer_native false @@ -210,9 +219,34 @@ section ServerM mpState := headerParserState data := SnapshotData.headerData cmdState } + return (headerSnap, srcSearchPath) + + def initializeWorker (p : DidOpenTextDocumentParams) (i o e : FS.Stream) + : IO ServerContext := do + let doc := p.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 (headerSnap, srcSearchPath) ← compileHeader meta o let cancelTk ← CancelToken.new - let cmdSnaps ← unfoldCmdSnaps m headerSnap cancelTk - (←read).docRef.set ⟨m, headerSnap, cmdSnaps, cancelTk⟩ + let cmdSnaps ← unfoldCmdSnaps meta headerSnap cancelTk o + let doc : EditableDocument := ⟨meta, headerSnap, cmdSnaps, cancelTk⟩ + return { + hIn := i + hOut := o + hLog := e + srcSearchPath := srcSearchPath + docRef := ←IO.mkRef doc + pendingRequestsRef := ←IO.mkRef RBMap.empty + } +end Initialization + +section Updates + def updatePendingRequests (map : PendingRequestMap → PendingRequestMap) : ServerM Unit := do + (←read).pendingRequestsRef.modify map /-- Given the new document and `changePos`, the UTF-8 offset of a change into the pre-change source, updates editable doc state. -/ @@ -239,7 +273,7 @@ section ServerM let mut validSnaps := cmdSnaps.finishedPrefix.takeWhile (fun s => s.endPos < changePos) if validSnaps.length = 0 then let cancelTk ← CancelToken.new - let newCmdSnaps ← unfoldCmdSnaps newMeta newHeaderSnap cancelTk + let newCmdSnaps ← unfoldCmdSnaps newMeta newHeaderSnap cancelTk st.hOut st.docRef.set ⟨newMeta, newHeaderSnap, newCmdSnaps, cancelTk⟩ else /- When at least one valid non-header snap exists, it may happen that a change does not fall @@ -257,23 +291,14 @@ section ServerM validSnaps ← validSnaps.dropLast lastSnap ← preLastSnap let cancelTk ← CancelToken.new - let newSnaps ← unfoldCmdSnaps newMeta lastSnap cancelTk + let newSnaps ← unfoldCmdSnaps newMeta lastSnap cancelTk st.hOut let newCmdSnaps := AsyncList.ofList validSnaps ++ newSnaps st.docRef.set ⟨newMeta, newHeaderSnap, newCmdSnaps, cancelTk⟩ -end ServerM +end Updates /- Notifications are handled in the main thread. They may change global worker state such as the current file contents. -/ section NotificationHandling - def handleDidOpen (p : DidOpenTextDocumentParams) : ServerM Unit := - let doc := p.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. -/ - compileDocument ⟨doc.uri, doc.version, doc.text.toFileMap⟩ - def handleDidChange (p : DidChangeTextDocumentParams) : ServerM Unit := do let docId := p.textDocument let changes := p.contentChanges @@ -529,17 +554,9 @@ def initAndRunWorker (i o e : FS.Stream) : IO UInt32 := do let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams let e ← e.withPrefix s!"[{param.textDocument.uri}] " let _ ← IO.setStderr e - let ctx : ServerContext := { - hIn := i - hOut := o - hLog := e - -- `openDocument` will not access `docRef`, but set it - docRef := ←IO.mkRef arbitrary - pendingRequestsRef := ←IO.mkRef (RBMap.empty : PendingRequestMap) - } - ReaderT.run (r := ctx) try - handleDidOpen param - mainLoop + try + let ctx ← initializeWorker param i o e + ReaderT.run (r := ctx) mainLoop return 0 catch e => o.writeLspNotification {