diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-19 14:13:20 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-26 14:07:36 +0100 |
| commit | aa7c872724e0d9bb79520152d613085c92d67236 (patch) | |
| tree | ffae52d3a2428903ced9432c0049f3b8d34dc298 /tactics/inv.ml | |
| parent | 545ab8b8439366877b3b40b49c483b9b61c85298 (diff) | |
STM: when an error occurs in a worker send back a bunch of states
In this way when the user fixes the script only a small part of
the broken proof has to be recomputed on master. The density of
states sent back decreases as they get far from the error. I.e.
counting from the error, the worker sends back states at distance
0 1 2 3 5 7 10 14 19 26 35 47...
Diffstat (limited to 'tactics/inv.ml')
0 files changed, 0 insertions, 0 deletions