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.

source
@[reducible, inline]
abbrev ProofWidgets.RequestId :
Type
Equations

- ProofWidgets.RequestId = Nat

Instances For

source
structure ProofWidgets.CancellableTask :
Type

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

Instances For

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

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

source
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.

Instances For

source
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.

Instances For

source
inductive ProofWidgets.CheckRequestResponse :
Type

The status of a running cancellable request.

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

Instances For

source
instance ProofWidgets.instRpcEncodableCheckRequestResponse :
Lean.Server.RpcEncodable CheckRequestResponse
Equations

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

source
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.

Instances For

source
def ProofWidgets.cancellableSuffix :
Lean.Name
Equations

- ProofWidgets.cancellableSuffix = `_cancellable

Instances For