Experimental support for cancellable RPC requests.

Note: Cancellation should eventually become a feature of the core RPC protocol, and the requests map should be stored in RequestM, or somewhere in the server anyway.

@[reducible, inline]

abbrev ProofWidgets.RequestId : Type

Equations

• ProofWidgets.RequestId = Nat

structure ProofWidgets.CancellableTask : Type

• task : Task (Except Lean.Server.RequestError (LazyEncodable Lean.Json))
• cancel : IO Unit

opaque ProofWidgets.runningRequests : IO.Ref (RequestId × Std.HashMap RequestId CancellableTask)

Maps the ID of each currently executing request to its task.

def ProofWidgets.mkCancellable {β : Type} {α : Sort u_1} [Lean.Server.RpcEncodable β] (handler : α → Lean.Server.RequestM (Lean.Server.RequestTask β)) : α → Lean.Server.RequestM (Lean.Server.RequestTask RequestId)

Transforms a request handler returning β into one that returns immediately with a RequestId.

The ID uniquely identifies the running request: its results can be retrieved using checkRequest, and it can be cancelled using cancelRequest.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.cancelRequest (rid : RequestId) : Lean.Server.RequestM (Lean.Server.RequestTask String)

Cancel the request with ID rid. Does nothing if rid is invalid.

Equations

• One or more equations did not get rendered due to their size.

inductive ProofWidgets.CheckRequestResponse : Type

The status of a running cancellable request.

• running : CheckRequestResponse
• done (result : LazyEncodable Lean.Json) : CheckRequestResponse

instance ProofWidgets.instRpcEncodableCheckRequestResponse : Lean.Server.RpcEncodable CheckRequestResponse

Equations

• ProofWidgets.instRpcEncodableCheckRequestResponse = { rpcEncode := ProofWidgets.instRpcEncodableCheckRequestResponse.enc✝, rpcDecode := ProofWidgets.instRpcEncodableCheckRequestResponse.dec✝ }

def ProofWidgets.checkRequest (rid : RequestId) : Lean.Server.RequestM (Lean.Server.RequestTask CheckRequestResponse)

Check whether a request has finished computing, and return the response if so. The request is removed from runningRequests the first time it is checked and found to have finished. Throws an error if the rid is invalid, or if the request itself threw an error.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.cancellableSuffix : Lean.Name

Equations

• ProofWidgets.cancellableSuffix = `_cancellable