ITP: makes replay work interactively in IDE

src/session/controller_itp.ml

@@ -573,7 +573,7 @@ let schedule_proof_attempt c id pr ~limit ~callback ~notification =
         update_proof_node notification c id false
     | _ -> ())
   in
-  schedule_proof_attempt_r c id pr ~limit:limit ~callback
+  schedule_proof_attempt_r c id pr ~limit ~callback
 
 let schedule_transformation_r c id name args ~callback =
   let apply_trans () =
@@ -773,21 +773,19 @@ let copy_detached ~copy c from_any =
   | _ -> raise (BadCopyDetached "copy_detached. Can only copy goal")
 
 
-let replay_proof_attempt c pr limit (id: proofNodeID) ~callback =
-
+let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notification =
   (* The replay can be done on a different machine so we need
      to check more things before giving the attempt to the scheduler *)
   if not (Hprover.mem c.controller_provers pr) then
-    callback (Uninstalled pr)
+    callback id (Uninstalled pr)
   else
-    (Queue.add (c, id, pr, limit, callback) scheduled_proof_attempts;
-     callback Scheduled;
-     run_timeout_handler ())
+    schedule_proof_attempt c parid pr ~limit ~callback ~notification
 
 type report =
   | Result of Call_provers.prover_result * Call_provers.prover_result
   (** Result(new_result,old_result) *)
   | CallFailed of exn
+  | Replay_interrupted
   | Prover_not_installed
   | Edited_file_absent of string
   | No_former_result of Call_provers.prover_result
@@ -799,8 +797,10 @@ let print_report fmt (r: report) =
     Format.fprintf fmt "new_result = %a, old_result = %a@."
       Call_provers.print_prover_result new_r
       Call_provers.print_prover_result old_r
-  | CallFailed _ ->
-    Format.fprintf fmt "Callfailed@."
+  | CallFailed e ->
+    Format.fprintf fmt "Callfailed %a@." Exn_printer.exn_printer e
+  | Replay_interrupted ->
+    Format.fprintf fmt "Interrupted@."
   | Prover_not_installed ->
     Format.fprintf fmt "Prover not installed@."
   | Edited_file_absent _ ->
@@ -818,21 +818,25 @@ let replay_print fmt (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_
   in
   Format.fprintf fmt "%a@." (Pp.print_list Pp.newline pp_elem) lr
 
-let replay ~remove_obsolete ~use_steps c ~callback =
+let replay ~remove_obsolete ~use_steps c ~callback ~notification ~final_callback =
 
   (* === Side functions used by replay === *)
   let counting s count =
     match s with
-    | Interrupted -> count := !count - 1
-    | Done _ -> count := !count - 1
-    | InternalFailure _ -> count := !count - 1
+    | Scheduled | Running -> ()
+    | Unedited | JustEdited -> assert false
+    | Interrupted
+    | Done _
+    | InternalFailure _
     | Uninstalled _ -> count := !count - 1
-    | _ -> () in
+  in
 
   let craft_report s r id pr limits pa =
     match s with
-    | Interrupted -> assert false
-(* Never happen r := (id, pr, limits, CallFailed (User_interrupt)) :: !r *)
+    | Scheduled | Running -> ()
+    | Unedited | JustEdited -> assert false
+    | Interrupted ->
+       r := (id, pr, limits, Replay_interrupted ) :: !r
     | Done new_r ->
         (match pa.Session_itp.proof_state with
         | None -> (r := (id, pr, limits, No_former_result new_r) :: !r)
@@ -840,9 +844,10 @@ let replay ~remove_obsolete ~use_steps c ~callback =
     | InternalFailure e ->
         r := (id, pr, limits, CallFailed (e)) :: !r
     | Uninstalled _ -> r := (id, pr, limits, Prover_not_installed) :: !r;
-    | _ -> () in
+  in
 
-  let update_node pa s =
+(*
+  let update_node pa s callback =
     match s with
     | Done new_r ->
         (pa.Session_itp.proof_state <- Some new_r;
@@ -851,7 +856,8 @@ let replay ~remove_obsolete ~use_steps c ~callback =
         pa.proof_obsolete <- true
     | Uninstalled _ ->
         pa.proof_obsolete <- true
-    | _ -> () in
+    | _ -> assert false in
+ *)
 
   let update_uninstalled c remove_obsolete id s pr =
     match s with
@@ -873,8 +879,8 @@ let replay ~remove_obsolete ~use_steps c ~callback =
     (fun _ _ -> count := !count + 1) session;
 
   (* Replaying function *)
-  let replay_pa pa =
-    let id = pa.parent in
+  let replay_pa id pa =
+    let parid = pa.parent in
     let pr = pa.prover in
     (* If use_steps, we give only steps as a limit *)
     let limit =
@@ -883,16 +889,19 @@ let replay ~remove_obsolete ~use_steps c ~callback =
       else
         pa.limit
     in
-    replay_proof_attempt c pr limit id
-      ~callback:(fun s ->
+    replay_proof_attempt c pr limit parid id
+      ~callback:(fun id s ->
         counting s count;
-        craft_report s report id pr limit pa;
-        update_node pa s;
-        update_uninstalled c remove_obsolete id s pr;
-        if !count = 0 then callback !report) in
+        craft_report s report parid pr limit pa;
+(*
+        update_node pa s ~callback ~notification;
+ *)
+        update_uninstalled c remove_obsolete parid s pr;
+        callback id s;
+        if !count = 0 then final_callback !report)
+      ~notification in
 
   (* Calling replay on all the proof_attempts of the session *)
-  Session_itp.session_iter_proof_attempt
-    (fun _ pa -> replay_pa pa) session
+  Session_itp.session_iter_proof_attempt replay_pa session
 
 end

src/session/controller_itp.mli

@@ -236,6 +236,7 @@ type report =
   | Result of Call_provers.prover_result * Call_provers.prover_result
         (** Result(new_result,old_result) *)
   | CallFailed of exn
+  | Replay_interrupted
   | Prover_not_installed
   | Edited_file_absent of string
   | No_former_result of Call_provers.prover_result
@@ -255,7 +256,9 @@ val replay:
         some cases: for example when prover is not installed *)
     use_steps:bool -> (** Replay use recorded number of proof steps if true *)
     controller ->
-    callback:
+    callback:(proofAttemptID -> proof_attempt_status -> unit) ->
+    notification:(any -> bool -> unit) ->
+    final_callback:
       ((proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list
             -> unit) ->
     unit

src/session/itp_server.ml

@@ -934,10 +934,12 @@ let () =
 
   let replay_session () : unit =
     let d = get_server_data () in
-    let callback = fun lr ->
+    let callback = callback_update_tree_proof d.cont in
+    let final_callback lr =
       P.notify (Message (Replay_Info (Pp.string_of C.replay_print lr))) in
     (* TODO make replay print *)
-    C.replay ~use_steps:false d.cont ~callback:callback ~remove_obsolete:false
+    C.replay ~use_steps:false ~remove_obsolete:false d.cont
+             ~callback ~notification:notify_change_proved ~final_callback
 
   (* ---------------- Mark obsolete ------------------ *)
   let mark_obsolete n =
@@ -1036,7 +1038,7 @@ let () =
     | Save_file_req (name, text)   ->
         save_file name text;
     | Get_task nid                 -> send_task nid
-    | Replay_req                   -> replay_session (); reload_session ()
+    | Replay_req                   -> replay_session ()
     | Interrupt_req                -> C.interrupt ()
     | Command_req (nid, cmd)       ->
       begin

src/session/session_itp.mli

@@ -65,7 +65,7 @@ type proof_attempt_node = {
   proof_script        : string option;  (* non empty for external ITP *)
 }
 
-val session_iter_proof_attempt: (proofNodeID -> proof_attempt_node -> unit) -> session -> unit
+val session_iter_proof_attempt: (proofAttemptID -> proof_attempt_node -> unit) -> session -> unit
 
 (* [is_below s a b] true if a is below b in the session tree *)
 val is_below: session -> any -> any -> bool