package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
val async_proofs_flags_for_workers : string list 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 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 (T : Task) () : sig ... end

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

exception RemoteException of Pp.t

convenience exception to marshall to master

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct