diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-27 17:41:37 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-30 17:29:33 +0100 |
| commit | 7516c468528c83593fe4094db35502bc2cda94f8 (patch) | |
| tree | 128aad3ea9f62ebd603fcfc41c7a0a478cb1aaea /toplevel | |
| parent | 1059ecce2a2662e4d8f335bd4db743df70b100b1 (diff) | |
STM: tell the user if the master is recomputing states validated by workers
When the worker fails, the master may need to recompute some states
the worker has already validates. In this case they are colored
accordingly.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/stm.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index ac041a9f7..3f0c23277 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1308,6 +1308,8 @@ let known_state ?(redefine_qed=false) ~cache id = inject_non_pstate s ), cache in + if !Flags.async_proofs_mode = Flags.APonParallel 0 then + Pp.feedback ~state_id:id Interface.ProcessingInMaster; State.define ~cache:cache_step ~redefine:redefine_qed step id; prerr_endline ("reached: "^ Stateid.to_string id) in reach ~redefine_qed id |