Skip to content

Commit

Permalink
fix: make IO-bound tasks dedicated (#5678)
Browse files Browse the repository at this point in the history
This PR ensures that all I/O-bound tasks in the language server use
dedicated tasks.
  • Loading branch information
mhuisi authored Oct 11, 2024
1 parent 087219b commit a3bc4d2
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
4 changes: 2 additions & 2 deletions src/Lean/Server/FileWorker.lean
Original file line number Diff line number Diff line change
Expand Up @@ -569,7 +569,7 @@ section MessageHandling
let text := st.doc.meta.text

match st.importCachingTask? with
| none => IO.asTask do
| none => IO.asTask (prio := Task.Priority.dedicated) do
let availableImports ← ImportCompletion.collectAvailableImports
let lastRequestTimestampMs ← IO.monoMsNow
let completions := ImportCompletion.find text st.doc.initSnap.stx params availableImports
Expand Down Expand Up @@ -697,7 +697,7 @@ end MainLoop

def runRefreshTask : WorkerM (Task (Except IO.Error Unit)) := do
let ctx ← read
IO.asTask do
IO.asTask (prio := Task.Priority.dedicated) do
while ! (←IO.checkCanceled) do
let pastProcessingStates ← ctx.chanIsProcessing.recvAllCurrent
if pastProcessingStates.isEmpty then
Expand Down
4 changes: 2 additions & 2 deletions src/Lean/Server/Watchdog.lean
Original file line number Diff line number Diff line change
Expand Up @@ -995,7 +995,7 @@ section MainLoop
/- Runs asynchronously. -/
let msg ← st.hIn.readLspMessage
pure <| ServerEvent.clientMsg msg
let clientTask := (← IO.asTask readMsgAction).map fun
let clientTask := (← IO.asTask (prio := Task.Priority.dedicated) readMsgAction).map fun
| Except.ok ev => ev
| Except.error e => ServerEvent.clientError e
return clientTask
Expand Down Expand Up @@ -1161,7 +1161,7 @@ results in requests that need references.
def startLoadingReferences (references : IO.Ref References) : IO Unit := do
-- Discard the task; there isn't much we can do about this failing,
-- but we should try to continue server operations regardless
let _ ← IO.asTask do
let _ ← IO.asTask (prio := Task.Priority.dedicated) do
let oleanSearchPath ← Lean.searchPathRef.get
for path in ← oleanSearchPath.findAllWithExt "ilean" do
try
Expand Down

0 comments on commit a3bc4d2

Please sign in to comment.