feat: improve handling of interrupt exceptions in the server

src/Lean/CoreM.lean

@@ -440,7 +440,7 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 @[inline] def CoreM.toIO (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do
   match (← (x.run { ctx with initHeartbeats := (← IO.getNumHeartbeats) } s).toIO') with
   | Except.error (Exception.error _ msg)   => throw <| IO.userError (← msg.toString)
-  | Except.error (Exception.internal id _) => throw <| IO.userError <| "internal exception #" ++ toString id.idx
+  | Except.error (Exception.internal id _) => throw <| IO.userError (← id.getDescription)
   | Except.ok a                            => return a
 
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=

src/Lean/Data/JsonRpc.lean

@@ -63,7 +63,7 @@ inductive ErrorCode where
   If a client decides that a result is not of any use anymore
   the client should cancel the request. -/
   | contentModified
-  /-- The client has canceled a request and a server as detected the cancel. -/
+  /-- The client has cancelled a request and the server has detected the cancel. -/
   | requestCancelled
   -- Lean-specific codes below.
   | rpcNeedsReconnect

src/Lean/Elab/BuiltinCommand.lean

@@ -492,7 +492,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     hasNoErrorMessages
   catch
     | ex@(Exception.error _ _) => do logException ex; pure false
-    | Exception.internal id _  => do logError (← id.getName); pure false
+    | Exception.internal id _  => do logError (← id.getDescription); pure false
   finally
     restoreMessages prevMessages
   if succeeded then

src/Lean/Elab/DocString/Builtin.lean

@@ -786,7 +786,7 @@ instance : Append DocCode where
 
 
 private partial def highlightSyntax
-    [Monad m] [MonadLiftT IO m]
+    [Monad m] [MonadLiftT (EIO Exception) m]
     (trees : PersistentArray InfoTree) (stx : Syntax) : m DocCode := do
   (go stx).run {} <&> (·.2)
 where

src/Lean/Elab/InfoTree/Main.lean

@@ -113,29 +113,32 @@ def InfoState.substituteLazy (s : InfoState) : Task InfoState :=
     lazyAssignment := {}
   }
 
-/-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`. -/
-def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
+/-- Embeds a `CoreM` action in `EIO` by supplying the information stored in `info`. -/
+def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α)
+    (cancelTk? : Option IO.CancelToken := none) : EIO Exception α := do
   -- We assume that this function is used only outside elaboration, mostly in the language server,
   -- and so we can and should provide access to information regardless whether it is exported.
   let env := info.env.setExporting false
   /-
     We must execute `x` using the `ngen` stored in `info`. Otherwise, we may create `MVarId`s and `FVarId`s that
     have been used in `lctx` and `info.mctx`.
   -/
-  (·.1) <$>
-    (withOptions (fun _ => info.options) x).toIO
-      { currNamespace := info.currNamespace, openDecls := info.openDecls
-        fileName := "<InfoTree>", fileMap := default }
-      { env, ngen := info.ngen }
+  (withOptions (fun _ => info.options) x).run'
+    { currNamespace := info.currNamespace, openDecls := info.openDecls
+      fileName := "<InfoTree>", fileMap := default, cancelTk? }
+    { env, ngen := info.ngen }
 
-def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
-  (·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })
+def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α)
+    (cancelTk? : Option IO.CancelToken := none) :
+    EIO Exception α := do
+  info.runCoreM (x.run' { lctx := lctx } { mctx := info.mctx }) cancelTk?
 
 def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPContext :=
   { env  := info.env, mctx := info.mctx, lctx := lctx,
     opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls }
 
-def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format := do
+def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) :
+    BaseIO Format :=
   ppTerm (info.toPPContext lctx) ⟨stx⟩  -- HACK: might not be a term
 
 private def formatStxRange (ctx : ContextInfo) (stx : Syntax) : Format :=
@@ -155,10 +158,10 @@ private def formatElabInfo (ctx : ContextInfo) (info : ElabInfo) : Format :=
   else
     f!"{formatStxRange ctx info.stx} @ {info.elaborator}"
 
-def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO α :=
+def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : EIO Exception α :=
   ctx.runMetaM info.lctx x
 
-def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
+def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : EIO Exception Format := do
   info.runMetaM ctx do
     let ty : Format ←
       try
@@ -170,39 +173,39 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
 def PartialTermInfo.format (ctx : ContextInfo) (info : PartialTermInfo) : Format :=
   f!"[PartialTerm] @ {formatElabInfo ctx info.toElabInfo}"
 
-def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
+def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : EIO Exception Format :=
   match info with
   | .dot i (expectedType? := expectedType?) .. => return f!"[Completion-Dot] {← i.format ctx} : {expectedType?}"
   | .id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[Completion-Id] {← ctx.ppSyntax lctx stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
   | _ => return f!"[Completion] {info.stx} @ {formatStxRange ctx info.stx}"
 
-def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
-  return f!"[Command] @ {formatElabInfo ctx info.toElabInfo}"
+def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : Format :=
+  f!"[Command] @ {formatElabInfo ctx info.toElabInfo}"
 
-def OptionInfo.format (ctx : ContextInfo) (info : OptionInfo) : IO Format := do
-  return f!"[Option] {info.optionName} @ {formatStxRange ctx info.stx}"
+def OptionInfo.format (ctx : ContextInfo) (info : OptionInfo) : Format :=
+  f!"[Option] {info.optionName} @ {formatStxRange ctx info.stx}"
 
-def ErrorNameInfo.format (ctx : ContextInfo) (info : ErrorNameInfo) : IO Format := do
-  return f!"[ErrorName] {info.errorName} @ {formatStxRange ctx info.stx}"
+def ErrorNameInfo.format (ctx : ContextInfo) (info : ErrorNameInfo) : Format :=
+  f!"[ErrorName] {info.errorName} @ {formatStxRange ctx info.stx}"
 
-def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do
+def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : EIO Exception Format := do
   ctx.runMetaM info.lctx do
     return f!"[Field] {info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}"
 
-def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format :=
+def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : EIO Exception Format :=
   if goals.isEmpty then
     return "no goals"
   else
     ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM (Meta.ppGoal ·)))
 
-def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do
+def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : EIO Exception Format := do
   let ctxB := { ctx with mctx := info.mctxBefore }
   let ctxA := { ctx with mctx := info.mctxAfter }
   let goalsBefore ← ctxB.ppGoals info.goalsBefore
   let goalsAfter  ← ctxA.ppGoals info.goalsAfter
   return f!"[Tactic] @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
 
-def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do
+def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : BaseIO Format := do
   let stx    ← ctx.ppSyntax info.lctx info.stx
   let output ← ctx.ppSyntax info.lctx info.output
   return f!"[MacroExpansion]\n{stx}\n===>\n{output}"
@@ -216,16 +219,16 @@ def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"[FieldRedecl] @ {formatStxRange ctx info.stx}"
 
-def DelabTermInfo.docString? (ppCtx : PPContext) (info : DelabTermInfo) : IO (Option String) := do
+def DelabTermInfo.docString? (ppCtx : PPContext) (info : DelabTermInfo) :
+    BaseIO (Option String) := do
   match info.mkDocString? with
   | none => return none
   | some act =>
-    try
-      act ppCtx
-    catch ex =>
-      return s!"[Error: {ex.toString}]"
+    match ← (act ppCtx).toBaseIO with
+    | .ok v => return v
+    | .error ex => return s!"[Error: {ex.toString}]"
 
-def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do
+def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : EIO Exception Format := do
   let loc := if let some loc := info.location? then f!"{loc.module} {loc.range.pos}-{loc.range.endPos}" else "none"
   let docString? ← info.docString? (ctx.toPPContext info.lctx)
   return f!"[DelabTerm] @ {← TermInfo.format ctx info.toTermInfo}\n\
@@ -242,14 +245,14 @@ def DocInfo.format (ctx : ContextInfo) (info : DocInfo) : Format :=
 def DocElabInfo.format (ctx : ContextInfo) (info : DocElabInfo) : Format :=
   f!"[DocElab] {info.name} ({repr info.kind}) @ {formatElabInfo ctx info.toElabInfo}"
 
-def Info.format (ctx : ContextInfo) : Info → IO Format
+def Info.format (ctx : ContextInfo) : Info → EIO Exception Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
   | ofPartialTermInfo i    => pure <| i.format ctx
-  | ofCommandInfo i        => i.format ctx
+  | ofCommandInfo i        => pure <| i.format ctx
   | ofMacroExpansionInfo i => i.format ctx
-  | ofOptionInfo i         => i.format ctx
-  | ofErrorNameInfo i      => i.format ctx
+  | ofOptionInfo i         => pure <| i.format ctx
+  | ofErrorNameInfo i      => pure <| i.format ctx
   | ofFieldInfo i          => i.format ctx
   | ofCompletionInfo i     => i.format ctx
   | ofUserWidgetInfo i     => pure <| i.format
@@ -304,7 +307,8 @@ def PartialContextInfo.format (ctx : PartialContextInfo) : Format :=
   | .parentDeclCtx n => s!"parent[{n}]"
   | .autoImplicitCtx implicits => s!"autoImplicits[{implicits}]"
 
-partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format := do
+partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) :
+    EIO Exception Format := do
   match tree with
   | hole id     => return .nestD f!"• ?{toString id.name}"
   | context i t => format t <| i.mergeIntoOuter? ctx?

src/Lean/Elab/Util.lean

@@ -237,8 +237,7 @@ def logException [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [
   | Exception.error ref msg => logErrorAt ref msg
   | Exception.internal id _ =>
     unless isAbortExceptionId id || ex.isInterrupt do
-      let name ← id.getName
-      logError m!"internal exception: {name}"
+      logError (← id.getDescription)
 
 /--
 If `x` throws an exception, catch it and turn it into a log message (using `logException`).

src/Lean/InternalExceptionId.lean

@@ -47,4 +47,8 @@ def InternalExceptionId.getName (id : InternalExceptionId) : IO Name :=  do
   else
     throw <| IO.userError "invalid internal exception id"
 
+/-- Return a description containing the internal exception's name. -/
+def InternalExceptionId.getDescription (id : InternalExceptionId) : IO String :=
+  return s!"internal exception: {← id.getName}"
+
 end Lean

src/Lean/Linter/List.lean

@@ -207,7 +207,8 @@ def allowedArrayNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs"
 def allowedVectorNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs", "ds", "acc"]
 
 /-- Find all binders appearing in the given info tree. -/
-def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) : IO (List (Syntax × Name × Expr)) :=
+def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) :
+    EIO Exception (List (Syntax × Name × Expr)) :=
   t.collectTermInfoM fun ctx ti => do
     if ti.isBinder then do
       -- Something is wrong here: sometimes `inferType` fails with an unknown fvar error,

src/Lean/Server/CodeActions/UnknownIdentifier.lean

@@ -137,7 +137,7 @@ def computeDotQuery?
     (doc : EditableDocument)
     (ctx : Elab.ContextInfo)
     (ti : Elab.TermInfo)
-    : IO (Option Query) := do
+    : EIO Exception (Option Query) := do
   let text := doc.meta.text
   let some pos := ti.stx.getPos? (canonicalOnly := true)
     | return none
@@ -173,7 +173,7 @@ def computeDotIdQuery?
     (id : Name)
     (lctx : LocalContext)
     (expectedType? : Option Expr)
-    : IO (Option Query) := do
+    : EIO Exception (Option Query) := do
   let some pos := stx.getPos? (canonicalOnly := true)
     | return none
   let some tailPos := stx.getTailPos? (canonicalOnly := true)
@@ -277,6 +277,7 @@ def handleUnknownIdentifierCodeAction
   }
   let r ← ServerTask.waitAny [
     responseTask.mapCheap Sum.inl,
+    -- TODO: does this intentionally ignore edit-based cancellations?
     rc.cancelTk.requestCancellationTask.mapCheap Sum.inr
   ]
   let .inl (.success response) := r

src/Lean/Server/Completion/CompletionCollectors.lean

@@ -542,7 +542,7 @@ def optionCompletion
     (ctx               : ContextInfo)
     (stx               : Syntax)
     (caps              : ClientCapabilities)
-    : IO (Array ResolvableCompletionItem) :=
+    : EIO Exception (Array ResolvableCompletionItem) :=
   ctx.runMetaM {} do
     -- HACK(WN): unfold the type so ForIn works
     let (decls : Std.TreeMap _ _ _) ← getOptionDecls
@@ -569,7 +569,7 @@ def errorNameCompletion
     (ctx               : ContextInfo)
     (partialId         : Syntax)
     (caps              : ClientCapabilities)
-    : IO (Array ResolvableCompletionItem) :=
+    : EIO Exception (Array ResolvableCompletionItem) :=
   ctx.runMetaM {} do
     let explanations ← getErrorExplanations
     return trailingDotCompletion explanations partialId caps ctx fun name explan textEdit? => {
@@ -596,7 +596,7 @@ def tacticCompletion
     (pos               : Lsp.Position)
     (completionInfoPos : Nat)
     (ctx               : ContextInfo)
-    : IO (Array ResolvableCompletionItem) := ctx.runMetaM .empty do
+    : EIO Exception (Array ResolvableCompletionItem) := ctx.runMetaM .empty do
   -- Don't include tactics that are identified only by their internal parser name
   let allTacticDocs ← Tactic.Doc.allTacticDocs (includeUnnamed := false)
   let items : Array ResolvableCompletionItem := allTacticDocs.map fun tacticDoc => {
@@ -643,7 +643,7 @@ def endSectionCompletion
     (id?               : Option Name)
     (danglingDot       : Bool)
     (scopeNames        : List String)
-    : IO (Array ResolvableCompletionItem) := do
+    : BaseIO (Array ResolvableCompletionItem) := do
   let mut idComponents := id?.map (fun id => id.components.toArray.map (·.toString)) |>.getD #[]
   if danglingDot then
     idComponents := idComponents.push ""

src/Lean/Server/Completion/CompletionResolution.lean

@@ -95,7 +95,7 @@ def resolveCompletionItem?
     (item              : CompletionItem)
     (id                : CompletionIdentifier)
     (completionInfoPos : Nat)
-    : IO CompletionItem := do
+    : EIO Exception CompletionItem := do
   let (completionInfos, _) := findCompletionInfosAt fileMap hoverPos cmdStx infoTree
   let some i := completionInfos[completionInfoPos]?
     | return item

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -130,15 +130,15 @@ def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
       let filter ctx info _ results := do
         let .ofTermInfo ti := info
           | return results
-        ctx.runMetaM info.lctx do
+        ctx.runMetaM info.lctx (cancelTk? := ← (← read).cancelTk.cancelTk) do
           results.filterM fun (_, r) => do
             let .ofTermInfo childTi := r.info
               | return true
             return ! (← isInstanceProjectionInfoFor kind ti childTi)
-      let some info ← snap.infoTree.hoverableInfoAtM? (m := IO) hoverPos
+      let some info ← snap.infoTree.hoverableInfoAtM? (m := RequestM) hoverPos
           (includeStop := true) (filter := filter)
         | return #[]
-      locationLinksOfInfo doc.meta kind info snap.infoTree
+      locationLinksOfInfo doc.meta kind info snap.infoTree (← (← read).cancelTk.cancelTk)
 
 open Language in
 def findGoalsAt? (doc : EditableDocument) (hoverPos : String.Pos.Raw) : ServerTask (Option (List Elab.GoalsAtResult)) :=
@@ -193,13 +193,13 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
       let ciAfter := { ci with mctx := ti.mctxAfter }
       let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
       -- compute the interactive goals
-      let goals ← ci.runMetaM {} (do
+      let goals ← ci.runMetaM {} (cancelTk? := ← (← read).cancelTk.cancelTk) (do
         let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
         let goals ← goals.mapM Widget.goalToInteractive
         return ⟨goals⟩
       )
       -- compute the goal diff
-      ciAfter.runMetaM {} (do
+      ciAfter.runMetaM {} (cancelTk? := ← (← read).cancelTk.cancelTk) (do
           try
             Widget.diffInteractiveGoals useAfter ti goals
           catch _ =>
@@ -231,11 +231,11 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
   mapTaskCostly (findInfoTreeAtPos doc hoverPos (includeStop := true)) <| Option.bindM fun infoTree => do
     let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := infoTree.termGoalAt? hoverPos
       | return none
-    let ty ← ci.runMetaM i.lctx do
+    let ty ← ci.runMetaM i.lctx (cancelTk? := ← (← read).cancelTk.cancelTk) do
       instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
     -- for binders, hide the last hypothesis (the binder itself)
     let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
-    let goal ← ci.runMetaM lctx' do
+    let goal ← ci.runMetaM lctx' (cancelTk? := ← (← read).cancelTk.cancelTk) do
       Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
     let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
     return some { goal with range, term := ← WithRpcRef.mk ti }

src/Lean/Server/FileWorker/SignatureHelp.lean

@@ -18,7 +18,7 @@ namespace Lean.Server.FileWorker.SignatureHelp
 open Lean
 
 def determineSignatureHelp (tree : Elab.InfoTree) (appStx : Syntax)
-    : IO (Option Lsp.SignatureHelp) := do
+    : EIO Exception (Option Lsp.SignatureHelp) := do
   let some (appCtx, .ofTermInfo appInfo) := tree.smallestInfo? fun
       | .ofTermInfo ti =>
         -- HACK: Use range of syntax to figure out corresponding `TermInfo`.
@@ -97,7 +97,8 @@ private def isPositionInLineComment (text : FileMap) (pos : String.Pos.Raw) : Bo
 
 open CandidateKind in
 def findSignatureHelp? (text : FileMap) (ctx? : Option Lsp.SignatureHelpContext) (cmdStx : Syntax)
-    (tree : Elab.InfoTree) (requestedPos : String.Pos.Raw) : IO (Option Lsp.SignatureHelp) := do
+    (tree : Elab.InfoTree) (requestedPos : String.Pos.Raw) :
+    EIO Exception (Option Lsp.SignatureHelp) := do
   -- HACK: Since comments are whitespace, the signature help can trigger on comments.
   -- This is especially annoying on end-of-line comments, as the signature help will trigger on
   -- every space in the comment.