| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | *Queue: API to wake up all threads |  Enrico Tassi | 2015-02-16 |
| | | |||
| * | Update headers. |  Maxime Dénès | 2015-01-12 |
| | | |||
| * | AsyncTaskQueue: simpler model (no parking area, continuation tasks) | Enrico Tassi | 2014-12-17 |
| | | |||
| * | AsyncTaskQueue: parsin can also happen in the workers now | Enrico Tassi | 2014-11-27 |
| | | |||
| * | AsyncTaskQueue: API to park a worker | Enrico Tassi | 2014-11-27 |
| | | | | | | | | | | | | | 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. | ||
| * | STM: code refactoring | Enrico Tassi | 2014-11-03 |
| | | | | | | This is mainly shuffling code around and removing internal refs that are not needed anymore. | ||
| * | STM: primitives to snapshot a .vi while in interactive mode | Enrico Tassi | 2014-10-13 |
| | | |||
| * | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | 2014-08-05 |
| | | | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2). | ||
| * | STM: code restructured to reuse task queue for tactics | Enrico Tassi | 2014-08-05 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |