perf: cancel redundant interactive requests (#746)

This PR ensures that the infoview cancels interactive goal/term
goal/diagnostic/widget requests when they are no longer needed (e.g.
because the user moved their cursor away).

- Also cancel `infoToInteractive` (popup contents),
`lazyTraceChildrenToInteractive` (trace explorer contents), and
`msgToInteractive` (message contents).
- Remove the `autoCancel` RPC call option. I think it was a mistake and
we should just auto-cancel all requests when the infoview closes.
- Cleanup `useAsyncWithTrigger` slightly.

Author: Vtec234

lean4-infoview-api/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview-api",
-    "version": "0.12.0",
+    "version": "0.13.0",
     "description": "Types and API for @leanprover/infoview.",
     "repository": {
         "type": "git",

lean4-infoview-api/src/infoviewApi.ts

@@ -61,10 +61,6 @@ export interface ClientRequestOptions {
      * Does nothing if the promise has already been resolved or rejected.
      */
     abortSignal?: AbortSignal
-    /**
-     * If `true`, the request will be automatically cancelled when the infoview is closed.
-     */
-    autoCancel?: boolean
 }
 
 /** Interface that the InfoView WebView uses to talk to the hosting editor. */

lean4-infoview-api/src/rpcApi.ts

@@ -6,6 +6,7 @@
  */
 
 import type { LocationLink, Position, Range, TextDocumentPositionParams } from 'vscode-languageserver-protocol'
+import { ClientRequestOptions } from './infoviewApi'
 import { LeanDiagnostic, RpcPtr } from './lspTypes'
 import { RpcSessionAtPos } from './rpcSessions'
 
@@ -85,15 +86,17 @@ export interface InteractiveGoals {
 export function getInteractiveGoals(
     rs: RpcSessionAtPos,
     pos: TextDocumentPositionParams,
+    options?: ClientRequestOptions,
 ): Promise<InteractiveGoals | undefined> {
-    return rs.call('Lean.Widget.getInteractiveGoals', pos)
+    return rs.call('Lean.Widget.getInteractiveGoals', pos, options)
 }
 
 export function getInteractiveTermGoal(
     rs: RpcSessionAtPos,
     pos: TextDocumentPositionParams,
+    options?: ClientRequestOptions,
 ): Promise<InteractiveTermGoal | undefined> {
-    return rs.call('Lean.Widget.getInteractiveTermGoal', pos)
+    return rs.call('Lean.Widget.getInteractiveTermGoal', pos, options)
 }
 
 export type Name = string
@@ -125,43 +128,59 @@ export interface LineRange {
 export function getInteractiveDiagnostics(
     rs: RpcSessionAtPos,
     lineRange?: LineRange,
+    options?: ClientRequestOptions,
 ): Promise<InteractiveDiagnostic[]> {
-    return rs.call('Lean.Widget.getInteractiveDiagnostics', { lineRange })
+    return rs.call('Lean.Widget.getInteractiveDiagnostics', { lineRange }, options)
 }
 
 export function InteractiveDiagnostics_msgToInteractive(
     rs: RpcSessionAtPos,
     msg: MessageData,
     indent: number,
+    options?: ClientRequestOptions,
 ): Promise<TaggedText<MsgEmbed>> {
     interface MessageToInteractive {
         msg: MessageData
         indent: number
     }
-    return rs.call<MessageToInteractive, TaggedText<MsgEmbed>>('Lean.Widget.InteractiveDiagnostics.msgToInteractive', {
-        msg,
-        indent,
-    })
+    return rs.call<MessageToInteractive, TaggedText<MsgEmbed>>(
+        'Lean.Widget.InteractiveDiagnostics.msgToInteractive',
+        {
+            msg,
+            indent,
+        },
+        options,
+    )
 }
 
 export function lazyTraceChildrenToInteractive(
     rs: RpcSessionAtPos,
     children: LazyTraceChildren,
+    options?: ClientRequestOptions,
 ): Promise<TaggedText<MsgEmbed>[]> {
-    return rs.call('Lean.Widget.lazyTraceChildrenToInteractive', children)
+    return rs.call('Lean.Widget.lazyTraceChildrenToInteractive', children, options)
 }
 
-export function InteractiveDiagnostics_infoToInteractive(rs: RpcSessionAtPos, info: InfoWithCtx): Promise<InfoPopup> {
-    return rs.call('Lean.Widget.InteractiveDiagnostics.infoToInteractive', info)
+export function InteractiveDiagnostics_infoToInteractive(
+    rs: RpcSessionAtPos,
+    info: InfoWithCtx,
+    options?: ClientRequestOptions,
+): Promise<InfoPopup> {
+    return rs.call('Lean.Widget.InteractiveDiagnostics.infoToInteractive', info, options)
 }
 
 export type GoToKind = 'declaration' | 'definition' | 'type'
-export function getGoToLocation(rs: RpcSessionAtPos, kind: GoToKind, info: InfoWithCtx): Promise<LocationLink[]> {
+export function getGoToLocation(
+    rs: RpcSessionAtPos,
+    kind: GoToKind,
+    info: InfoWithCtx,
+    options?: ClientRequestOptions,
+): Promise<LocationLink[]> {
     interface GetGoToLocationParams {
         kind: GoToKind
         info: InfoWithCtx
     }
-    return rs.call<GetGoToLocationParams, LocationLink[]>('Lean.Widget.getGoToLocation', { kind, info })
+    return rs.call<GetGoToLocationParams, LocationLink[]>('Lean.Widget.getGoToLocation', { kind, info }, options)
 }
 
 export interface UserWidget {
@@ -192,8 +211,12 @@ export interface UserWidgets {
 }
 
 /** Given a position, returns all of the user-widgets on the infotree at this position. */
-export function Widget_getWidgets(rs: RpcSessionAtPos, pos: Position): Promise<UserWidgets> {
-    return rs.call<Position, UserWidgets>('Lean.Widget.getWidgets', pos)
+export function Widget_getWidgets(
+    rs: RpcSessionAtPos,
+    pos: Position,
+    options?: ClientRequestOptions,
+): Promise<UserWidgets> {
+    return rs.call<Position, UserWidgets>('Lean.Widget.getWidgets', pos, options)
 }
 
 /** Code that should be dynamically loaded by the UserWidget component. */
@@ -208,12 +231,17 @@ export interface WidgetSource {
  *
  * We make the assumption that either the code doesn't exist, or it exists and does not change for the lifetime of the widget.
  */
-export function Widget_getWidgetSource(rs: RpcSessionAtPos, pos: Position, hash: string): Promise<WidgetSource> {
+export function Widget_getWidgetSource(
+    rs: RpcSessionAtPos,
+    pos: Position,
+    hash: string,
+    options?: ClientRequestOptions,
+): Promise<WidgetSource> {
     interface GetWidgetSourceParams {
         hash: string
         pos: Position
     }
-    return rs.call<GetWidgetSourceParams, WidgetSource>('Lean.Widget.getWidgetSource', { pos, hash })
+    return rs.call<GetWidgetSourceParams, WidgetSource>('Lean.Widget.getWidgetSource', { pos, hash }, options)
 }
 
 export type HighlightedSubexprInfo = SubexprInfo | 'highlighted'
@@ -244,9 +272,14 @@ export function highlightMatches(
     rs: RpcSessionAtPos,
     query: string,
     msg: TaggedText<MsgEmbed>,
+    options?: ClientRequestOptions,
 ): Promise<TaggedText<HighlightedMsgEmbed>> {
-    return rs.call<HighlightMatchesParams, TaggedText<HighlightedMsgEmbed>>('Lean.Widget.highlightMatches', {
-        query,
-        msg,
-    })
+    return rs.call<HighlightMatchesParams, TaggedText<HighlightedMsgEmbed>>(
+        'Lean.Widget.highlightMatches',
+        {
+            query,
+            msg,
+        },
+        options,
+    )
 }

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.12.0",
+    "version": "0.13.0",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "repository": {
         "type": "git",
@@ -57,7 +57,7 @@
         "typescript": "^5.4.5"
     },
     "dependencies": {
-        "@leanprover/infoview-api": "~0.12.0",
+        "@leanprover/infoview-api": "~0.13.0",
         "@vscode/codicons": "^0.0.40",
         "@vscode-elements/react-elements": "^0.5.0",
         "es-module-lexer": "^1.5.4",

lean4-infoview/src/index.tsx

@@ -30,7 +30,10 @@ export { MessageData }
 /** Display the given message data as interactive, pretty-printed text. */
 export function InteractiveMessageData({ msg }: { msg: MessageData }) {
     const rs = useRpcSession()
-    const interactive = useAsync(() => InteractiveDiagnostics_msgToInteractive(rs, msg, 0), [rs, msg])
+    const interactive = useAsync(
+        abortSignal => InteractiveDiagnostics_msgToInteractive(rs, msg, 0, { abortSignal }),
+        [rs, msg],
+    )
 
     if (interactive.state === 'resolved') {
         return <InteractiveMessage fmt={interactive.value} />

lean4-infoview/src/infoview/info.tsx

@@ -509,12 +509,16 @@ function InfoAux(props: InfoProps) {
     // with e.g. a new `pos`.
     type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'>
     const [state, triggerUpdateCore] = useAsyncWithTrigger(
-        () =>
+        abortSignal =>
             new Promise<InfoRequestResult>((resolve, reject) => {
-                const goalsReq = getInteractiveGoals(rpcSess, DocumentPosition.toTdpp(pos))
-                const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos))
-                const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound)
-                const messagesReq = getInteractiveDiagnostics(rpcSess, { start: pos.line, end: pos.line + 1 })
+                const goalsReq = getInteractiveGoals(rpcSess, DocumentPosition.toTdpp(pos), { abortSignal })
+                const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos), { abortSignal })
+                const widgetsReq = Widget_getWidgets(rpcSess, pos, { abortSignal }).catch(discardMethodNotFound)
+                const messagesReq = getInteractiveDiagnostics(
+                    rpcSess,
+                    { start: pos.line, end: pos.line + 1 },
+                    { abortSignal },
+                )
                     // fall back to non-interactive diagnostics when lake fails
                     // (see https://github.com/leanprover/vscode-lean4/issues/90)
                     .then(diags => (diags.length === 0 ? lspDiagsHere.map(lspDiagToInteractive) : diags))
@@ -566,6 +570,12 @@ function InfoAux(props: InfoProps) {
                             reject('retry')
                             return
                         }
+                        // When `ex?.code === RpcErrorCode.RequestCancelled`,
+                        // we fall through to resolving with an error below.
+                        // - In case we were cancelled by `useAsyncWithTrigger`,
+                        //   `resolve` will do nothing.
+                        // - We should not be cancelled otherwise,
+                        //   and if that happens it is an error that should be displayed.
 
                         let errorString = ''
                         if (typeof ex === 'string') {

lean4-infoview/src/infoview/interactiveCode.tsx

@@ -114,7 +114,10 @@ function TypePopupContents({ info }: TypePopupContentsProps) {
     // When `err` is defined we show the error,
     // otherwise if `ip` is defined we show its contents,
     // otherwise a 'loading' message.
-    const interactive = useAsync(() => InteractiveDiagnostics_infoToInteractive(rs, info.info), [rs, info.info])
+    const interactive = useAsync(
+        abortSignal => InteractiveDiagnostics_infoToInteractive(rs, info.info, { abortSignal }),
+        [rs, info.info],
+    )
 
     // Even when subexpressions are selectable in our parent component, it doesn't make sense
     // to select things inside the *type* of the parent, so we clear the context.

lean4-infoview/src/infoview/traceExplorer.tsx

@@ -52,13 +52,16 @@ function ChildlessTraceNode(traceEmbed: HighlightedTraceEmbed) {
 function CollapsibleTraceNode(traceEmbed: HighlightedTraceEmbed) {
     const { cls, collapsed: collapsedByDefault, children: lazyKids } = traceEmbed
     const rs = useRpcSession()
-    const [children, fetchChildren] = useAsyncWithTrigger(async () => {
-        if ('strict' in lazyKids) {
-            return lazyKids.strict
-        } else {
-            return lazyTraceChildrenToInteractive(rs, lazyKids.lazy)
-        }
-    }, [rs, lazyKids])
+    const [children, fetchChildren] = useAsyncWithTrigger(
+        async abortSignal => {
+            if ('strict' in lazyKids) {
+                return lazyKids.strict
+            } else {
+                return lazyTraceChildrenToInteractive(rs, lazyKids.lazy, { abortSignal })
+            }
+        },
+        [rs, lazyKids],
+    )
 
     const [open, setOpen] = React.useState(!collapsedByDefault)
     if (open && children.state === 'notStarted') void fetchChildren()