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...

1 files changed, 26 insertions, 9 deletions

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 4f8149229..e7597a1b7 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -206,6 +206,7 @@ module VCS : sig
   val reached : id -> bool -> unit
   val goals : id -> int -> unit
   val set_state : id -> state -> unit
+  val get_state : id -> state option
   val forget_state : id -> unit
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
@@ -359,6 +360,7 @@ end = struct (* {{{ *)
     | Some x -> x
     | None -> raise Vcs_aux.Expired
   let set_state id s = (get_info id).state <- Some s
+  let get_state id = (get_info id).state
   let forget_state id = (get_info id).state <- None
   let reached id b =
     let info = get_info id in
@@ -554,7 +556,7 @@ end = struct (* {{{ *)
     with VCS.Expired -> anomaly (str "not a cached state (expired)")
 
   let assign id s =
-    try VCS.set_state id s
+    try if VCS.get_state id = None then VCS.set_state id s
     with VCS.Expired -> ()
 
   let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
@@ -680,8 +682,9 @@ end = struct (* {{{ *)
 
   type response =
     | RespBuiltProof of Entries.proof_output list * float
-    | RespError of (* err, safe, msg, safe_state *)
-        Stateid.t * Stateid.t * std_ppcmds * State.frozen_state option
+    | RespError of (* err, safe, msg, safe_states *)
+        Stateid.t * Stateid.t * std_ppcmds *
+          (Stateid.t * State.frozen_state) list
     | RespFeedback of Interface.feedback
     | RespGetCounterFreshLocalUniv
     | RespGetCounterNewUnivLevel
@@ -967,10 +970,10 @@ end = struct (* {{{ *)
                 last_task := None;
                 raise KillRespawn
             | TaskBuildProof(_,_,_, assign,_,_,_,_),
-              RespError(err_id,valid,e,s) ->
+              RespError(err_id,valid,e,valid_states) ->
                 let e = Stateid.add ~valid (RemoteException e) err_id in
                 assign (`Exn e);
-                Option.iter (State.assign valid) s;
+                List.iter (fun (id,s) -> State.assign id s) valid_states;
                 (* We restart the slave, to avoid memory leaks.  We could just
                    Pp.feedback (Interface.InProgress ~-1) *)
                 last_task := None;
@@ -1110,10 +1113,24 @@ end = struct (* {{{ *)
         prerr_endline (string_of_ppcmds (print e));
         prerr_endline ("last safe id is: " ^ Stateid.to_string safe_id);
         prerr_endline ("cached? " ^ string_of_bool (State.is_cached safe_id));
-        let state =
-          if State.is_cached safe_id then Some (State.get_cached safe_id)
-          else None in
-        marshal_response !slave_oc (RespError (err_id, safe_id, print e, state))
+        let prog old_v n =
+          if n < 3 then n else old_v + n/3 + if n mod 3 > 0 then 1 else 0 in
+        let states =
+          let open State in
+          let rec aux n m prev_id =
+            let next =
+              try Some (VCS.visit prev_id).next
+              with VCS.Expired -> None in
+            match next with
+            | None -> []
+            | Some id when n = m ->
+                prerr_endline ("sending back state " ^  string_of_int m);
+                let tail = aux (n+1) (prog m (n+1)) id in
+                if is_cached id then (id, get_cached id) :: tail else tail
+            | Some id -> aux (n+1) m id in
+          (if is_cached safe_id then [safe_id,get_cached safe_id] else [])
+          @ aux 1 (prog 1 1) safe_id in
+        marshal_response !slave_oc (RespError(err_id, safe_id, print e, states))
       | e ->
         pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
         flush_all (); exit 1