aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorEnrico Tassi2014-11-26 19:05:38 +0100
committerEnrico Tassi2014-11-27 16:06:54 +0100
commitf549ddbb9fae979d4b7b260316ea4754f2c28ffa (patch)
tree12e254fbf260fc8c8844a7de74848816b00fdc82 /kernel/nativecode.ml
parent5f7234edcf0a6bef995c8d1dc31f679799a98557 (diff)
AsyncTaskQueue: API to park a worker
Generalize the old model by letting one park a worker and by letting the (parked) worker be picky about the tasks it picks up. The use of that is the following: a proof worker, while performing its "main" task (building a proof term) computes all the intermediate states but returns only its main result. One can ask the worker to hang around, and react to special tasks, like printing the goals of an intermediate state.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions