| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Update headers following #6543. |  Théo Zimmermann | 2018-02-27 |
| | | |||
| * | Fix mli-doc issue #6531 |  Tony Beta Lambda | 2018-01-01 |
| | | |||
| * | [flags] [stm] Reorganize flags. |  Emilio Jesus Gallego Arias | 2017-12-11 |
| | | | | | | | | | We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag. | ||
| * | [stm] [doc] Add some documentation to AsyncTaskQueue API | Emilio Jesus Gallego Arias | 2017-11-21 |
| | | | | | | As a bonus we remove some trailing whitespace, and implement a couple of hints suggested in the discussion. | ||
| * | Fix FIXME: use OCaml 4.02 generative functors when available. |  Gaëtan Gilbert | 2017-11-01 |
| | | | | | 4.02.3 has been the minimal OCaml version for a while now. | ||
| * | Bump year in headers. |  Pierre-Marie Pédrot | 2017-07-04 |
| | | |||
| * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| | | |||
| * | *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 |