package coq

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

Module Stm.QueryTaskSource

Sourcetype task

Main description of a task. Elements are stored in the "master" process, and then converted into a request.

Sourcetype competence

competence stores the information about what kind of work a worker has completed / has available.

Sourcetype worker_status =
  1. | Fresh
  2. | Old of competence

A worker_status is:

  • `Fresh when a worker is born.
  • `Old of competence: When a worker ends a job it can either die (and be replaced by a fresh new worker) or hang there as an `Old worker. In such case some data can be carried by the `Old constructor, typically used to implement request_of_task.

This allows to implement both one-shot workers and "persistent" ones. E.g. par: is implement using workers that don't "reboot". Proof workers do reboot mainly because the vm has some C state that cannot be cleared, so you have a real memory leak if you don't reboot the worker.

Sourcetype request

Type of input and output data for workers.

The data must be marshallable as it send through the network using Marshal .

Sourcetype response
Sourceval name : string ref

UID of the task kind

Sourceval extra_env : unit -> string array

Extra arguments of the task kind

Master API, it is run by the master, on a thread
Sourceval request_of_task : worker_status -> task -> request option

request_of_task status t takes the status of the worker and a task t and creates the corresponding Some request to be sent to the worker or it is not valid anymore None.

Sourceval task_match : worker_status -> task -> bool

task_match status tid Allows to discard tasks based on the worker status.

Sourceval use_response : worker_status -> task -> response -> [ `Stay of competence * task list | `End ]

use_response status t out

For a response out to a task t with status we can choose to end the worker of to keep it alive with some data and immediately inject extra tasks in the queue.

For example, the proof worker runs a proof and finds an error, the response signals that, e.g.

ReponseError {state = 34; msg = "oops"}

When the manager uses such a response he can tell the worker to stay there and inject into the queue an extra task requesting state 33 (to implement efficient proof repair).

Sourceval on_marshal_error : string -> task -> unit

on_marshal_error err_msg tid notifies of marshaling failure.

Sourceval on_task_cancellation_or_expiration_or_slave_death : task option -> unit

on_task_cancellation_or_expiration_or_slave_death tid

These functions are meant to parametrize the worker manager on the actions to be taken when things go wrong or are cancelled (you can kill a worker in CoqIDE, or using kill -9...)

E.g. master can decide to inhabit the (delegate) Future.t with a closure (to be run in master), i.e. make the document still checkable. This is what I do for marshaling errors.

Sourceval forward_feedback : Feedback.feedback -> unit

forward_feedback fb sends fb to all the workers.

Worker API, it is run by worker, on a different fresh process
Sourceval perform : request -> response

perform in synchronously processes a request in

Sourceval name_of_task : task -> string

debugging

Sourceval name_of_request : request -> string
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