fix: restore synchronous fast-forwarding path in language processor (l…

…eanprover#5802)

Between leanprover#3106 and this, it was possible that reparsing the file up to
the current position was stuck waiting in the threadpool queue,
displaying a yellow bar and not displaying any info on the unchanged
prefix.

src/Lean/Language/Lean.lean

@@ -300,7 +300,9 @@ General notes:
 * We must make sure to trigger `oldCancelTk?` as soon as discarding `old?`.
 * Control flow up to finding the last still-valid snapshot (which should be quick) is synchronous so
   as not to report this "fast forwarding" to the user as well as to make sure the next run sees all
-  fast-forwarded snapshots without having to wait on tasks.
+  fast-forwarded snapshots without having to wait on tasks. It also ensures this part cannot be
+  delayed by threadpool starvation. We track whether we are still on the fast-forwarding path using
+  the `sync` parameter on `parseCmd` and spawn an elaboration task when we leave it.
 -/
 partial def process
     (setupImports : Syntax → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
@@ -330,7 +332,7 @@ where
                 -- elaboration reuse
                 oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
                   let prom ← IO.Promise.new
-                  let _ ← IO.asTask (parseCmd oldCmd newParserState oldProcSuccess.cmdState prom ctx)
+                  parseCmd oldCmd newParserState oldProcSuccess.cmdState prom (sync := true) ctx
                   return .pure {
                     diagnostics := oldProcessed.diagnostics
                     result? := some {
@@ -446,7 +448,7 @@ where
       let parserState := Runtime.markPersistent parserState
       let cmdState := Runtime.markPersistent cmdState
       let ctx := Runtime.markPersistent ctx
-      let _ ← IO.asTask (parseCmd none parserState cmdState prom ctx)
+      parseCmd none parserState cmdState prom (sync := true) ctx
       return {
         diagnostics
         infoTree? := cmdState.infoState.trees[0]!
@@ -457,36 +459,22 @@ where
       }
 
   parseCmd (old? : Option CommandParsedSnapshot) (parserState : Parser.ModuleParserState)
-      (cmdState : Command.State) (prom : IO.Promise CommandParsedSnapshot) :
+      (cmdState : Command.State) (prom : IO.Promise CommandParsedSnapshot) (sync : Bool) :
       LeanProcessingM Unit := do
     let ctx ← read
 
-    -- check for cancellation, most likely during elaboration of previous command, before starting
-    -- processing of next command
-    if (← ctx.newCancelTk.isSet) then
-      -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
-      -- (as no-one should look at this result in that case) but anything containing `Environment`
-      -- is not `Inhabited`
-      prom.resolve <| .mk (nextCmdSnap? := none) {
-        diagnostics := .empty, stx := .missing, parserState
-        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
-        finishedSnap := .pure { diagnostics := .empty, cmdState }
-        tacticCache := (← IO.mkRef {})
-      }
-      return
-
     let unchanged old newParserState : BaseIO Unit :=
       -- when syntax is unchanged, reuse command processing task as is
       -- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still
       -- have changed because of trailing whitespace and comments etc., so it is passed separately
       -- from `old`
       if let some oldNext := old.nextCmdSnap? then do
         let newProm ← IO.Promise.new
-        let _ ← old.data.finishedSnap.bindIO fun oldFinished =>
+        let _ ← old.data.finishedSnap.bindIO (sync := true) fun oldFinished =>
           -- also wait on old command parse snapshot as parsing is cheap and may allow for
           -- elaboration reuse
           oldNext.bindIO (sync := true) fun oldNext => do
-            parseCmd oldNext newParserState oldFinished.cmdState newProm ctx
+            parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx
             return .pure ()
         prom.resolve <| .mk (data := old.data) (nextCmdSnap? := some { range? := none, task := newProm.result })
       else prom.resolve old  -- terminal command, we're done!
@@ -521,44 +509,61 @@ where
       if let some tk := ctx.oldCancelTk? then
         tk.set
 
-    -- definitely resolved in `doElab` task
-    let elabPromise ← IO.Promise.new
-    let finishedPromise ← IO.Promise.new
-    -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
-    -- retract the progress bar to a previous position in case the command support incremental
-    -- reporting but has significant work after resolving its last incremental promise, such as
-    -- final type checking; if it does not support incrementality, `elabSnap` constructed in
-    -- `parseCmd` and containing the entire range of the command will determine the reported
-    -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
-    -- irrelevant in this case.
-    let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
-    let finishedSnap := { range? := endRange?, task := finishedPromise.result }
-    let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
-
-    let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
-    let next? ← if Parser.isTerminalCommand stx then pure none
-      -- for now, wait on "command finished" snapshot before parsing next command
-      else some <$> IO.Promise.new
-    let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
-    let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
-      diagnostics
-      stx := .missing
-      parserState := {}
-      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-      finishedSnap
-      tacticCache
-    } else {
-      diagnostics, stx, parserState, tacticCache
-      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-      finishedSnap
-    }
-    prom.resolve <| .mk (nextCmdSnap? := next?.map
-      ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
-    let cmdState ← doElab stx cmdState beginPos
-      { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
-      finishedPromise tacticCache ctx
-    if let some next := next? then
-      parseCmd none parserState cmdState next ctx
+    -- check for cancellation, most likely during elaboration of previous command, before starting
+    -- processing of next command
+    if (← ctx.newCancelTk.isSet) then
+      -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
+      -- (as no-one should look at this result in that case) but anything containing `Environment`
+      -- is not `Inhabited`
+      prom.resolve <| .mk (nextCmdSnap? := none) {
+        diagnostics := .empty, stx := .missing, parserState
+        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
+        finishedSnap := .pure { diagnostics := .empty, cmdState }
+        tacticCache := (← IO.mkRef {})
+      }
+      return
+
+    -- Start new task when leaving fast-forwarding path; see "General notes" above
+    let _ ← (if sync then BaseIO.asTask else (.pure <$> ·)) do
+      -- definitely resolved in `doElab` task
+      let elabPromise ← IO.Promise.new
+      let finishedPromise ← IO.Promise.new
+      -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
+      -- retract the progress bar to a previous position in case the command support incremental
+      -- reporting but has significant work after resolving its last incremental promise, such as
+      -- final type checking; if it does not support incrementality, `elabSnap` constructed in
+      -- `parseCmd` and containing the entire range of the command will determine the reported
+      -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
+      -- irrelevant in this case.
+      let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
+      let finishedSnap := { range? := endRange?, task := finishedPromise.result }
+      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
+
+      let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
+      let next? ← if Parser.isTerminalCommand stx then pure none
+        -- for now, wait on "command finished" snapshot before parsing next command
+        else some <$> IO.Promise.new
+      let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
+      let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
+        diagnostics
+        stx := .missing
+        parserState := {}
+        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+        finishedSnap
+        tacticCache
+      } else {
+        diagnostics, stx, parserState, tacticCache
+        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+        finishedSnap
+      }
+      prom.resolve <| .mk (nextCmdSnap? := next?.map
+        ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
+      let cmdState ← doElab stx cmdState beginPos
+        { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
+        finishedPromise tacticCache ctx
+      if let some next := next? then
+        -- We're definitely off the fast-forwarding path now
+        parseCmd none parserState cmdState next (sync := false) ctx
 
   doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
       (snap : SnapshotBundle DynamicSnapshot) (finishedPromise : IO.Promise CommandFinishedSnapshot)
@@ -625,7 +630,7 @@ def processCommands (inputCtx : Parser.InputContext) (parserState : Parser.Modul
     (old? : Option (Parser.InputContext × CommandParsedSnapshot) := none) :
     BaseIO (Task CommandParsedSnapshot) := do
   let prom ← IO.Promise.new
-  process.parseCmd (old?.map (·.2)) parserState commandState prom
+  process.parseCmd (old?.map (·.2)) parserState commandState prom (sync := true)
     |>.run (old?.map (·.1))
     |>.run { inputCtx with }
   return prom.result