- hIn : IO.FS.Stream
- hOut : IO.FS.Stream
- hLog : IO.FS.Stream
- srcSearchPath : Lean.SearchPath
- initParams : Lean.Lsp.InitializeParams
- clientHasWidgets : Bool
- headerSnap : Lean.Server.Snapshots.Snapshot
- snaps : Array Lean.Server.Snapshots.Snapshot
@[inline]
def
Lean.Server.FileWorker.unfoldCmdSnaps
(m : Lean.Server.DocumentMeta)
(headerSnap : Lean.Server.Snapshots.Snapshot)
(snaps : Array Lean.Server.Snapshots.Snapshot)
(cancelTk : Lean.Server.FileWorker.CancelToken)
:
Equations
- Lean.Server.FileWorker.unfoldCmdSnaps m headerSnap snaps cancelTk = do let ctx ← read if (Array.isEmpty snaps && Lean.MessageLog.hasErrors (Lean.Server.Snapshots.Snapshot.msgLog headerSnap)) = true then do liftM (Lean.Server.publishProgressAtPos m headerSnap.beginPos ctx.hOut Lean.Lsp.LeanFileProgressKind.fatalError) liftM (Lean.Server.FileWorker.publishIleanInfoFinal m ctx.hOut #[headerSnap]) pure IO.AsyncList.nil else do liftM (Lean.Server.FileWorker.publishIleanInfoUpdate m ctx.hOut (Array.insertAt snaps 0 headerSnap)) liftM (IO.AsyncList.unfoldAsync (Lean.Server.FileWorker.nextCmdSnap ctx m cancelTk) { headerSnap := headerSnap, snaps := snaps })
@[inline]
Equations
- doc : Lean.Server.FileWorker.EditableDocument
- pendingRequests : Lean.Server.FileWorker.PendingRequestMap
- rpcSessions : Std.RBMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare
@[inline]
def
Lean.Server.FileWorker.lakeSetupSearchPath
(lakePath : System.FilePath)
(m : Lean.Server.DocumentMeta)
(imports : Array Lean.Import)
(hOut : IO.FS.Stream)
:
Equations
- Lean.Server.FileWorker.lakeSetupSearchPath lakePath m imports hOut = let args := #["print-paths"] ++ Array.map (fun a => toString a.module) imports; let cmdStr := String.intercalate " " (toString lakePath :: Array.toList args); do let lakeProc ← IO.Process.spawn { toStdioConfig := { stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }, cmd := lakePath.toString, args := args, cwd := none, env := #[] } (fun processStderr => do let stderr ← liftM (IO.asTask (processStderr "") Task.Priority.dedicated) let a ← IO.FS.Handle.readToEnd lakeProc.stdout let stdout : String := String.trim a let stderr ← IO.ofExcept stderr.get let a ← IO.Process.Child.wait lakeProc match a with | { val := Fin.ofNat 0 } => let stdout := List.getLast! (String.split stdout fun a => a == Char.ofNat 10); do let discr ← pure (Lean.Json.parse stdout >>= Lean.fromJson?) match discr with | Except.ok paths => do let a ← Lean.getBuildDir Lean.initSearchPath a paths.oleanPath Array.forM Lean.loadDynlib paths.loadDynlibPaths 0 (Array.size paths.loadDynlibPaths) List.mapM Lean.realPathNormalized paths.srcPath | x => IO.throwServerError (toString "invalid output from `" ++ toString cmdStr ++ toString "`:\n" ++ toString stdout ++ toString "\nstderr:\n" ++ toString stderr ++ toString "") | { val := Fin.ofNat 2 } => pure [] | x => IO.throwServerError (toString "`" ++ toString cmdStr ++ toString "` failed:\n" ++ toString stdout ++ toString "\nstderr:\n" ++ toString stderr ++ toString "")) (Lean.Server.FileWorker.lakeSetupSearchPath.processStderr lakePath m hOut args lakeProc)
partial def
Lean.Server.FileWorker.lakeSetupSearchPath.processStderr
(lakePath : System.FilePath)
(m : Lean.Server.DocumentMeta)
(hOut : IO.FS.Stream)
(args : Array String)
(lakeProc : IO.Process.Child
{ toStdioConfig :=
{ stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped },
cmd := lakePath.toString, args := args, cwd := none, env := #[] }.toStdioConfig)
(acc : String)
:
def
Lean.Server.FileWorker.compileHeader
(m : Lean.Server.DocumentMeta)
(hOut : IO.FS.Stream)
(opts : Lean.Options)
(hasWidgets : Bool)
:
Equations
-
Lean.Server.FileWorker.compileHeader m hOut opts hasWidgets = let inputCtx := Lean.Parser.mkInputContext m.text.source "";
do
let discr ← Lean.Parser.parseHeader inputCtx
let x : Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog := discr
match x with
| (headerStx, headerParserState, msgLog) => do
let a ← Lean.getBuildDir
let srcSearchPath ← Lean.initSrcSearchPath a ∅
let a ← liftM (IO.getEnv "LAKE")
let _do_jp : Lean.SearchPath → System.FilePath → IO (Lean.Server.Snapshots.Snapshot × Lean.SearchPath) :=
fun srcSearchPath lakePath =>
let _do_jp := fun srcSearchPath discr =>
let x := discr;
match x with
| (headerEnv, msgLog) =>
let headerEnv := headerEnv;
do
let r ←
tryCatch
(match Lean.Lsp.DocumentUri.toPath? m.uri with
| some path => do
let a ← Lean.moduleNameOfFileName path none
let headerEnv : Lean.Environment := Lean.Environment.setMainModule headerEnv a
let y ← pure PUnit.unit
pure { fst := y, snd := headerEnv }
| x => do
let y ← pure PUnit.unit
pure { fst := y, snd := headerEnv })
fun x => do
let y ← pure ()
pure { fst := y, snd := headerEnv }
let x : Lean.Environment := r.snd
let headerEnv : Lean.Environment := x
pure r.fst
let cmdState : Lean.Elab.Command.State := Lean.Elab.Command.mkState headerEnv msgLog opts
let cmdState : Lean.Elab.Command.State :=
{ env := cmdState.env, messages := cmdState.messages, scopes := cmdState.scopes,
nextMacroScope := cmdState.nextMacroScope, maxRecDepth := cmdState.maxRecDepth,
nextInstIdx := cmdState.nextInstIdx, ngen := cmdState.ngen,
infoState :=
{ enabled := true,
assignment :=
{ root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray,
size := 0 },
trees :=
Array.toPersistentArray
#[Lean.Elab.InfoTree.context
{ env := headerEnv, fileMap := m.text,
mctx :=
{ depth := 0, mvarCounter := 0,
lDepth :=
{ root :=
Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray,
size := 0 },
decls :=
{ root :=
Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray,
size := 0 },
userNames :=
{ root :=
Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray,
size := 0 },
lAssignment :=
{ root :=
Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray,
size := 0 },
eAssignment :=
{ root :=
Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray,
size := 0 },
dAssignment :=
{ root :=
Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray,
size := 0 } },
options := { entries := [] }, currNamespace := Lean.Name.anonymous, openDecls := [] }
(Lean.Elab.InfoTree.node
(Lean.Elab.Info.ofCommandInfo
{ toElabInfo := { elaborator := `header, stx := headerStx } })
(List.toPersistentArray
(List.map
(fun importStx =>
Lean.Elab.InfoTree.node
(Lean.Elab.Info.ofCommandInfo
{ toElabInfo := { elaborator := `import, stx := importStx } })
(Array.toPersistentArray #[]))
(Array.toList (Lean.Syntax.getArgs (Lean.Syntax.getOp headerStx 1))))))] },
traceState := cmdState.traceState }
let a ←
Std.PersistentArray.mapM (fun a => Lean.Widget.msgToInteractiveDiagnostic m.text a hasWidgets)
cmdState.messages.msgs
let headerSnap : Lean.Server.Snapshots.Snapshot :=
{ beginPos := 0, stx := headerStx, mpState := headerParserState, cmdState := cmdState,
interactiveDiags := a }
Lean.Server.publishDiagnostics m
(Std.PersistentArray.toArray (Lean.Server.Snapshots.Snapshot.diagnostics headerSnap)) hOut
pure (headerSnap, srcSearchPath);
do
let r ←
tryCatch
(let _do_jp := fun srcSearchPath y => do
let y ← Lean.Elab.processHeader headerStx opts msgLog inputCtx 0
pure { fst := y, snd := srcSearchPath };
match Lean.Lsp.DocumentUri.toPath? m.uri with
| some path => do
let a ← liftM (System.FilePath.pathExists lakePath)
if (System.FilePath.fileName path != some "lakefile.lean" && a) = true then do
let pkgSearchPath ←
Lean.Server.FileWorker.lakeSetupSearchPath lakePath m
(List.toArray (Lean.Elab.headerToImports headerStx)) hOut
let srcSearchPath : Lean.SearchPath := pkgSearchPath ++ srcSearchPath
let y ← pure PUnit.unit
_do_jp srcSearchPath y
else do
let y ← pure PUnit.unit
_do_jp srcSearchPath y
| x => do
let y ← pure PUnit.unit
_do_jp srcSearchPath y)
fun e =>
let msgs :=
Lean.MessageLog.add
{ fileName := "
" , pos := { line := 0, column := 0 }, endPos := none, severity := Lean.MessageSeverity.error, caption := "", data := Function.comp Lean.MessageData.ofFormat Lean.format (IO.Error.toString e) } Lean.MessageLog.empty; do let a ← Lean.mkEmptyEnvironment 0 let y ← pure (a, msgs) pure { fst := y, snd := srcSearchPath } let x : Lean.SearchPath := r.snd let srcSearchPath : Lean.SearchPath := x let y ← pure r.fst _do_jp srcSearchPath y match a with | some path => do let y ← pure { toString := path } _do_jp srcSearchPath y | none => do let a ← liftM (System.FilePath.pathExists { toString := "leanpkg.toml" }) let a_1 ← liftM (System.FilePath.pathExists { toString := "lakefile.lean" }) let lakePath : String := if (a && !a_1) = true then "leanpkg" else "lake" let a ← liftM (IO.getEnv "LEAN_SYSROOT") let _do_jp : System.FilePath → IO (Lean.Server.Snapshots.Snapshot × Lean.SearchPath) := fun lakePath => do let y ← pure (System.FilePath.withExtension lakePath System.FilePath.exeExtension) _do_jp srcSearchPath y match a with | some path => do let y ← pure ({ toString := path } / { toString := "bin" } / { toString := lakePath }) _do_jp y | x => do let a ← IO.appDir let y ← pure (a / { toString := lakePath }) _do_jp y
def
Lean.Server.FileWorker.initializeWorker
(meta : Lean.Server.DocumentMeta)
(i : IO.FS.Stream)
(o : IO.FS.Stream)
(e : IO.FS.Stream)
(initParams : Lean.Lsp.InitializeParams)
(opts : Lean.Options)
:
Equations
- Lean.Server.FileWorker.initializeWorker meta i o e initParams opts = let clientHasWidgets := Option.getD (Option.bind initParams.initializationOptions? fun a => a.hasWidgets?) false; do let discr ← Lean.Server.FileWorker.compileHeader meta o opts clientHasWidgets let x : Lean.Server.Snapshots.Snapshot × Lean.SearchPath := discr match x with | (headerSnap, srcSearchPath) => do let cancelTk ← Lean.Server.FileWorker.CancelToken.new let ctx : Lean.Server.FileWorker.WorkerContext := { hIn := i, hOut := o, hLog := e, srcSearchPath := srcSearchPath, initParams := initParams, clientHasWidgets := clientHasWidgets } let cmdSnaps ← Lean.Server.FileWorker.unfoldCmdSnaps meta headerSnap #[] cancelTk ctx let doc : Lean.Server.FileWorker.EditableDocument := { meta := meta, headerSnap := headerSnap, cmdSnaps := cmdSnaps, cancelTk := cancelTk } pure (ctx, { doc := doc, pendingRequests := Std.RBMap.empty, rpcSessions := Std.RBMap.empty })
def
Lean.Server.FileWorker.updatePendingRequests
(map : Lean.Server.FileWorker.PendingRequestMap → Lean.Server.FileWorker.PendingRequestMap)
:
Equations
- Lean.Server.FileWorker.updatePendingRequests map = modify fun st => { doc := st.doc, pendingRequests := map st.pendingRequests, rpcSessions := st.rpcSessions }
Equations
- Lean.Server.FileWorker.updateDocument newMeta = do let ctx ← read let a ← get let oldDoc : Lean.Server.FileWorker.EditableDocument := a.doc let newHeaderSnap ← liftM (Lean.Server.Snapshots.reparseHeader newMeta.text.source oldDoc.headerSnap { entries := [] }) let _do_jp : PUnit → Lean.Server.FileWorker.WorkerM Unit := fun y => do let discr ← liftM (IO.AsyncList.updateFinishedPrefix oldDoc.cmdSnaps) let x : IO.AsyncList Lean.Server.FileWorker.ElabTaskError Lean.Server.Snapshots.Snapshot × Option Lean.Server.FileWorker.ElabTaskError := discr match x with | (cmdSnaps, e?) => match e? with | some Lean.Server.FileWorker.ElabTaskError.aborted => liftM (IO.throwServerError "Internal server error: elab task was aborted while still in use.") | some (Lean.Server.FileWorker.ElabTaskError.ioError ioError) => throw ioError | x => do liftM (Lean.Server.FileWorker.CancelToken.set oldDoc.cancelTk) let changePos : String.Pos := String.firstDiffPos oldDoc.meta.text.source newMeta.text.source let validSnaps : List Lean.Server.Snapshots.Snapshot := List.takeWhile (fun s => decide (Lean.Server.Snapshots.Snapshot.endPos s < changePos)) (IO.AsyncList.finishedPrefix cmdSnaps) if List.length validSnaps = 0 then do let cancelTk ← liftM Lean.Server.FileWorker.CancelToken.new let newCmdSnaps ← liftM (Lean.Server.FileWorker.unfoldCmdSnaps newMeta newHeaderSnap #[] cancelTk ctx) modify fun st => { doc := { meta := newMeta, headerSnap := newHeaderSnap, cmdSnaps := newCmdSnaps, cancelTk := cancelTk }, pendingRequests := st.pendingRequests, rpcSessions := st.rpcSessions } else let lastSnap := List.getLast! validSnaps; let preLastSnap := if List.length validSnaps ≥ 2 then List.get! validSnaps (List.length validSnaps - 2) else newHeaderSnap; do let newLastStx ← liftM (Lean.Server.Snapshots.parseNextCmd newMeta.text.source preLastSnap) let _do_jp : List Lean.Server.Snapshots.Snapshot → PUnit → Lean.Server.FileWorker.WorkerM Unit := fun validSnaps y => do let cancelTk ← liftM Lean.Server.FileWorker.CancelToken.new let newSnaps ← liftM (Lean.Server.FileWorker.unfoldCmdSnaps newMeta newHeaderSnap (List.toArray validSnaps) cancelTk ctx) let newCmdSnaps : IO.AsyncList Lean.Server.FileWorker.ElabTaskError Lean.Server.Snapshots.Snapshot := IO.AsyncList.ofList validSnaps ++ newSnaps modify fun st => { doc := { meta := newMeta, headerSnap := newHeaderSnap, cmdSnaps := newCmdSnaps, cancelTk := cancelTk }, pendingRequests := st.pendingRequests, rpcSessions := st.rpcSessions } if (newLastStx != lastSnap.stx) = true then do let r ← pure (List.dropLast validSnaps) let validSnaps : List Lean.Server.Snapshots.Snapshot := r let y ← pure PUnit.unit _do_jp validSnaps y else do let y ← pure PUnit.unit _do_jp validSnaps y if (newHeaderSnap.stx != oldDoc.headerSnap.stx) = true then do let y ← liftM (IO.throwServerError "Internal server error: header changed but worker wasn't restarted.") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Server.FileWorker.handleDidChange p = let docId := p.textDocument; let changes := p.contentChanges; do let a ← get let oldDoc : Lean.Server.FileWorker.EditableDocument := a.doc let discr ← pure docId.version? match discr with | some newVersion => if newVersion ≤ oldDoc.meta.version then liftM (IO.eprintln (toString "Got outdated version number: " ++ toString newVersion ++ toString " ≤ " ++ toString oldDoc.meta.version ++ toString "")) else if ¬Array.isEmpty changes = true then let newDocText := Lean.Server.foldDocumentChanges changes oldDoc.meta.text; Lean.Server.FileWorker.updateDocument { uri := docId.uri, version := newVersion, text := newDocText } else pure PUnit.unit | x => liftM (IO.throwServerError "Expected version number")
Equations
- Lean.Server.FileWorker.handleCancelRequest p = Lean.Server.FileWorker.updatePendingRequests fun pendingRequests => Std.RBMap.erase pendingRequests p.id
Equations
- Lean.Server.FileWorker.handleRpcRelease p = do let st ← get match Std.RBMap.find? st.rpcSessions p.sessionId with | some seshRef => do let monoMsNow ← liftM IO.monoMsNow ST.Ref.modify seshRef fun sesh => Id.run (let sesh := sesh; do let r ← let col := p.refs; forIn col sesh fun ref r => let sesh := r; let sesh := (Lean.Server.FileWorker.RpcSession.release sesh ref).snd; do pure PUnit.unit pure (ForInStep.yield sesh) let x : Lean.Server.FileWorker.RpcSession := r let sesh : Lean.Server.FileWorker.RpcSession := x Lean.Server.FileWorker.RpcSession.keptAlive monoMsNow sesh) | x => pure PUnit.unit
Equations
- Lean.Server.FileWorker.handleRpcKeepAlive p = do let st ← get match Std.RBMap.find? st.rpcSessions p.sessionId with | none => pure PUnit.unit | some seshRef => do let a ← liftM IO.monoMsNow ST.Ref.modify seshRef fun a_1 => Lean.Server.FileWorker.RpcSession.keptAlive a a_1
Equations
- Lean.Server.FileWorker.handleRpcConnect p = do let discr ← liftM Lean.Server.FileWorker.RpcSession.new let x : UInt64 × Lean.Server.FileWorker.RpcSession := discr match x with | (newId, newSesh) => do let newSeshRef ← liftM (IO.mkRef newSesh) modify fun st => { doc := st.doc, pendingRequests := st.pendingRequests, rpcSessions := Std.RBMap.insert st.rpcSessions newId newSeshRef } pure { sessionId := newId }
def
Lean.Server.FileWorker.parseParams
(paramType : Type)
[inst : Lean.FromJson paramType]
(params : Lean.Json)
:
Lean.Server.FileWorker.WorkerM paramType
Equations
- Lean.Server.FileWorker.parseParams paramType params = match Lean.fromJson? params with | Except.ok parsed => pure parsed | Except.error inner => liftM (IO.throwServerError (toString "Got param with wrong structure: " ++ toString (Lean.Json.compress params) ++ toString "\n" ++ toString inner ++ toString ""))
Equations
- Lean.Server.FileWorker.handleNotification method params = let handle := fun paramType [Lean.FromJson paramType] handler => Lean.Server.FileWorker.parseParams paramType params >>= handler; match method with | "textDocument/didChange" => handle Lean.Lsp.DidChangeTextDocumentParams Lean.Server.FileWorker.handleDidChange | "$/cancelRequest" => handle Lean.Lsp.CancelParams Lean.Server.FileWorker.handleCancelRequest | "$/lean/rpc/release" => handle Lean.Lsp.RpcReleaseParams Lean.Server.FileWorker.handleRpcRelease | "$/lean/rpc/keepAlive" => handle Lean.Lsp.RpcKeepAliveParams Lean.Server.FileWorker.handleRpcKeepAlive | x => liftM (IO.throwServerError (toString "Got unsupported notification method: " ++ toString method ++ toString ""))
def
Lean.Server.FileWorker.queueRequest
(id : Lean.JsonRpc.RequestID)
(requestTask : Task (Except IO.Error Unit))
:
Equations
- Lean.Server.FileWorker.queueRequest id requestTask = Lean.Server.FileWorker.updatePendingRequests fun pendingRequests => Std.RBMap.insert pendingRequests id requestTask
def
Lean.Server.FileWorker.handleRequest
(id : Lean.JsonRpc.RequestID)
(method : String)
(params : Lean.Json)
:
Equations
- Lean.Server.FileWorker.handleRequest id method params = do let ctx ← read let st ← get let _do_jp : PUnit → Lean.Server.FileWorker.WorkerM Unit := fun y => let rc := { rpcSessions := st.rpcSessions, srcSearchPath := ctx.srcSearchPath, doc := st.doc, hLog := ctx.hLog, initParams := ctx.initParams }; do let t? ← liftM (EIO.toIO' (Lean.Server.handleLspRequest method params rc)) let _do_jp : Task (Except IO.Error Unit) → Lean.Server.FileWorker.WorkerM Unit := fun t₁ => Lean.Server.FileWorker.queueRequest id t₁ match t? with | Except.error e => do let y ← liftM (IO.asTask (IO.FS.Stream.writeLspResponseError ctx.hOut (Lean.Server.RequestError.toLspResponseError id e)) Task.Priority.default) _do_jp y | Except.ok t => do let y ← liftM ((fun a => IO.mapTask a t Task.Priority.default) fun x => match x with | Except.ok resp => IO.FS.Stream.writeLspResponse ctx.hOut { id := id, result := resp } | Except.error e => IO.FS.Stream.writeLspResponseError ctx.hOut (Lean.Server.RequestError.toLspResponseError id e)) _do_jp y if (method == "$/lean/rpc/connect") = true then do tryCatch (do let ps ← Lean.Server.FileWorker.parseParams Lean.Lsp.RpcConnectParams params let resp ← Lean.Server.FileWorker.handleRpcConnect ps liftM (IO.FS.Stream.writeLspResponse ctx.hOut { id := id, result := resp })) fun e => liftM (IO.FS.Stream.writeLspResponseError ctx.hOut { id := id, code := Lean.JsonRpc.ErrorCode.internalError, message := toString e, data? := none }) pure PUnit.unit else do let y ← pure PUnit.unit _do_jp y
def
Lean.Server.FileWorker.initAndRunWorker
(i : IO.FS.Stream)
(o : IO.FS.Stream)
(e : IO.FS.Stream)
(opts : Lean.Options)
:
Equations
- Lean.Server.FileWorker.initAndRunWorker i o e opts = do let i ← Lean.Server.maybeTee "fwIn.txt" false i let o ← Lean.Server.maybeTee "fwOut.txt" true o let initParams ← IO.FS.Stream.readLspRequestAs i "initialize" Lean.Lsp.InitializeParams let discr ← IO.FS.Stream.readLspNotificationAs i "textDocument/didOpen" Lean.Lsp.DidOpenTextDocumentParams let x : Lean.JsonRpc.Notification Lean.Lsp.DidOpenTextDocumentParams := discr match x with | { method := x, param := param } => let doc := param.textDocument; let meta := { uri := doc.uri, version := doc.version, text := String.toFileMap doc.text }; do let e ← pure (IO.FS.Stream.withPrefix e (toString "[" ++ toString param.textDocument.uri ++ toString "] ")) let discr ← liftM (IO.setStderr e) let x : IO.FS.Stream := discr match x with | x => do let r ← tryCatch (do let discr ← Lean.Server.FileWorker.initializeWorker meta i o e initParams.param opts let x : Lean.Server.FileWorker.WorkerContext × Lean.Server.FileWorker.WorkerState := discr match x with | (ctx, st) => do let discr ← StateRefT'.run (ReaderT.run Lean.Server.FileWorker.mainLoop ctx) st let x : Unit × Lean.Server.FileWorker.WorkerState := discr match x with | x => pure 0) fun e => do IO.eprintln e Lean.Server.publishDiagnostics meta #[{ range := { start := { line := 0, character := 0 }, end := { line := 0, character := 0 } }, fullRange := { start := { line := 0, character := 0 }, end := { line := 0, character := 0 } }, severity? := some Lean.Lsp.DiagnosticSeverity.error, code? := none, source? := none, message := IO.Error.toString e, tags? := none, relatedInformation? := none }] o pure 1 pure r
Equations
- Lean.Server.FileWorker.workerMain opts = do let i ← liftM IO.getStdin let o ← liftM IO.getStdout let e ← liftM IO.getStderr let r ← tryCatch (do let seed ← (UInt64.toNat ∘ ByteArray.toUInt64LE!) <$> IO.getRandomBytes 8 IO.setRandSeed seed let exitCode ← Lean.Server.FileWorker.initAndRunWorker i o e opts o.flush e.flush let y ← IO.Process.exit (UInt32.toUInt8 exitCode) pure (DoResultPR.pure y PUnit.unit)) fun err => do IO.FS.Stream.putStrLn e (toString "worker initialization error: " ++ toString err ++ toString "") pure (DoResultPR.return 1 PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure a | DoResultPR.return b u => let x := u; pure b