Module AsyncTaskQueue

val async_proofs_flags_for_workers : string list Stdlib.ref

This file provides an API for defining and managing a queue of tasks to be done by external workers.

A queue of items of type task is maintained, then for each task, a request is generated, then sent to a worker using marshalling.

The workers will then eventually return a result, using marshalling again: ____ ____ ____ ________ | T1 | T2 | T3 | => request => | Worker | |____|____|____| <= response <= |________| | Master Proc. | \--------------/

Thus request and response must be safely marshallable.

Operations for managing the task queue are provide, see below for more details.

module type Task = sig ... end

The Task module type defines an abstract message-processing queue.

type cancel_switch = bool Stdlib.ref

cancel_switch to be flipped to true by anyone to signal the task is not relevant anymore. When the STM performs an undo/edit-at, it crawls the document and flips these flags (the Qed node carries a pointer to the flag IIRC).

module MakeQueue (T : Task) () : sig ... end

Client-side functor. MakeQueue T creates a task queue for task T

module MakeWorker (_ : Task) () : sig ... end

Server-side functor. MakeWorker T creates the server task dispatcher.

exception RemoteException of Pp.t

convenience exception to marshall to master