aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/asyncTaskQueue.ml
Commit message (Collapse)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\
| * Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
| | | | | | | | Fixes compilation of Coq with OCaml 4.03 beta 1.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\|
| * workers: purge short version of -load-vernac too (fix #4458)Gravatar Enrico Tassi2016-01-04
| |
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
| | | | | | | | | | Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot.
* | Rich printing of messages.Gravatar Pierre-Marie Pédrot2015-09-20
|/
* *Queue: API to wake up all threadsGravatar Enrico Tassi2015-02-16
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Inlining Spawn.kill_if in the one place were it was actually used, thusGravatar Pierre-Marie Pédrot2014-12-25
| | | | removing the need of thread creation in the interface.
* CoqIDE: cleanup jobs window on worker deathGravatar Enrico Tassi2014-12-17
|
* AsyncTaskQueue: simpler model (no parking area, continuation tasks)Gravatar Enrico Tassi2014-12-17
|
* CThread: use a different type for thread friendly in_channelsGravatar Enrico Tassi2014-12-17
|
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
* AsyncTaskQueue: parsin can also happen in the workers nowGravatar Enrico Tassi2014-11-27
|
* AsyncTaskQueue: API to park a workerGravatar Enrico Tassi2014-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.
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
|
* STM: code refactoringGravatar Enrico Tassi2014-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 modeGravatar Enrico Tassi2014-10-13
|
* A marshalling failure does not make a worker `OldGravatar Enrico Tassi2014-09-09
|
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inGravatar Matthieu Sozeau2014-08-26
| | | | stm test-suite files.
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-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 tacticsGravatar Enrico Tassi2014-08-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 21:43:26 +0000