package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module AsyncTaskQueue.MakeQueueSource

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

Parameters

module T : Task

Signature

Sourcetype queue

queue is the abstract queue type.

Sourceval create : int -> CoqworkmgrApi.priority -> queue

create n pri will initialize the queue with n workers having priority pri. If n is 0, the queue won't spawn any process, working in a lazy local manner. not imposed by the this API

Sourceval destroy : queue -> unit

destroy q Deallocates q, cancelling all pending tasks.

Sourceval n_workers : queue -> int

n_workers q returns the number of workers of q

Sourceval enqueue_task : queue -> T.task -> cancel_switch:cancel_switch -> unit

enqueue_task q t ~cancel_switch schedules t for execution in q. cancel_switch can be flipped to true to cancel the task.

Sourceval join : queue -> unit

join q blocks until the task queue is empty

Sourceval cancel_all : queue -> unit

cancel_all q Cancels all tasks

Sourceval cancel_worker : queue -> WorkerPool.worker_id -> unit

cancel_worker q wid cancels a particular worker wid

Sourceval set_order : queue -> (T.task -> T.task -> int) -> unit

set_order q cmp reorders q using ordering cmp

Sourceval broadcast : queue -> unit

broadcast q

This is nasty. Workers can be picky, e.g. pick tasks only when they are "on screen". Of course the screen is scrolled, and that changes the potential choice of workers to pick up a task or not.

This function wakes up the workers (the managers) that give a look (again) to the tasks in the queue.

The STM calls it when the perspective (as in PIDE) changes.

A problem here is that why task_match has access to the competence data in order to decide if the task is palatable to the worker or not... such data is local to the worker (manager). The perspective is global, so it does not quite fit this picture. This API to make all managers reconsider the tasks in the queue is the best I could came up with.

This API is crucial to Coqoon (or any other UI that invokes Stm.finish eagerly but wants the workers to "focus" on the visible part of the document).

Sourceval snapshot : queue -> T.task list

snapshot q Takes a snapshot (non destructive but waits until all workers are enqueued)

Sourceval clear : queue -> unit

clear q Clears q, only if the worker prool is empty

Sourceval with_n_workers : int -> CoqworkmgrApi.priority -> (queue -> 'a) -> 'a

with_n_workers n pri f creates a queue, runs the function, destroys the queue. The user should call join

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