aboutsummaryrefslogtreecommitdiff
path: root/stm/workerPool.mli
AgeCommit message (Collapse)Author
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-17WorkerPool: simpler fuctor and no more parking areaEnrico Tassi
2014-11-27WorkerPool: API to move a worker from an active pool to a parking oneEnrico Tassi
This lets me have a pool of active workers of a fixed size, plus a parking area where workers that completed their job can stay holding their state (and eventually one can ask them to query such state afterwards).
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM.