STM: primitives to snapshot a .vi while in interactive mode

6 files changed, 75 insertions, 67 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 74e83a39f..22e7c0243 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -304,13 +304,19 @@ module Make(T : Task) = struct
         flush_all (); exit 1
     done
 
-  let dump () =
-    assert(WorkersPool.is_empty ()); (* ATM, we allow that only if no slaves *)
-    List.map fst (TQueue.dump queue)
+  let clear () =
+    assert(WorkersPool.is_empty ()); (* We allow that only if no slaves *)
+    TQueue.clear queue
+  
+  let snapshot () =
+    List.map fst
+     (TQueue.wait_until_n_are_waiting_then_snapshot
+       (WorkersPool.n_workers ()) queue)
 
   let init n =
     WorkersPool.init n manage_slave
       (fun n -> Printf.sprintf "%s:%d" T.name n)
+
   let destroy () =
     WorkersPool.destroy ();
     TQueue.destroy queue
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index ddbb28457..cd91ba129 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -61,6 +61,11 @@ module Make(T : Task) : sig
 
   val set_order : (T.task -> T.task -> int) -> unit
 
-  val dump : unit -> T.task list
+  (* Take a snapshot (non destructive but waits until all workers are
+   * enqueued) *)
+  val snapshot : unit -> T.task list
+
+  (* Clears the queue, only if the worker prool is empty *)
+  val clear : unit -> unit
 
 end
diff --git a/stm/stm.ml b/stm/stm.ml
index 5349b85a8..026866616 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -701,14 +701,6 @@ let record_pb_time proof_name loc time =
     hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
   end
  
-type 'a a_request = {
-  r_exn_info : Stateid.t * Stateid.t;
-  r_stop : Stateid.t;
-  r_document : VCS.vcs;
-  r_loc : Loc.t;
-  r_uuid     : 'a;
-  r_name     : string }
-
 exception RemoteException of std_ppcmds
 let _ = Errors.register_handler (function
   | RemoteException ppcmd -> ppcmd
@@ -730,7 +722,7 @@ module Task = struct
     t_uuid     : Future.UUID.t;
     t_name     : string }   
 
-  type request = Future.UUID.t a_request
+  type request = (Future.UUID.t,VCS.vcs) Stateid.request
   
   type error = {
     e_error_at    : Stateid.t;
@@ -746,17 +738,17 @@ module Task = struct
   let extra_env () = !async_proofs_workers_extra_env
 
   let name_of_task t = t.t_name
-  let name_of_request r = r.r_name
+  let name_of_request r = r.Stateid.name
 
   let request_of_task age { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name } =
    assert(age = `Fresh);
    try Some {
-     r_exn_info = t_exn_info;
-     r_stop = t_stop;
-     r_document = VCS.slice ~start:t_stop ~stop:t_start;
-     r_loc = t_loc;
-     r_uuid = t_uuid;
-     r_name = t_name }
+     Stateid.exn_info = t_exn_info;
+     stop = t_stop;
+     document = VCS.slice ~start:t_stop ~stop:t_start;
+     loc = t_loc;
+     uuid = t_uuid;
+     name = t_name }
    with VCS.Expired -> None
 
   let use_response { t_assign; t_loc; t_name } = function
@@ -795,13 +787,13 @@ module Task = struct
     Proof_global.return_proof ()
   let build_proof_here (id,valid) loc eop =
     Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop)
-  let perform { r_exn_info; r_stop = eop; r_document = vcs; r_loc } =
+  let perform { Stateid.exn_info; stop = eop; document = vcs; loc } =
     try
       VCS.restore vcs;
       VCS.print ();
       let rc, time =
         let wall_clock = Unix.gettimeofday () in
-        let l = Future.force (build_proof_here r_exn_info r_loc eop) in
+        let l = Future.force (build_proof_here exn_info loc eop) in
         l, Unix.gettimeofday () -. wall_clock in
       VCS.print ();
       RespBuiltProof(rc,time)
@@ -877,18 +869,19 @@ module Slaves : sig
   val slave_main_loop : (unit -> unit) -> unit
   val slave_init_stdout : unit -> unit
 
-  type tasks
-  val dump_final : int Future.UUIDMap.t -> tasks
-  val dump_snapshot : int Future.UUIDMap.t -> tasks
-  val check_task : string -> tasks -> int -> bool
-  val info_tasks : tasks -> (string * float * int) list
+  type 'a tasks = ('a,VCS.vcs) Stateid.request list
+  val dump_snapshot : unit -> Future.UUID.t tasks
+  val check_task : string -> int tasks -> int -> bool
+  val info_tasks : 'a tasks -> (string * float * int) list
   val finish_task :
     string ->
     Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
-    tasks -> int -> Library.seg_univ
+    int tasks -> int -> Library.seg_univ
 
   val cancel_worker : string -> unit
 
+  val reset_task_queue : unit -> unit
+
   val set_perspective : Stateid.t list -> unit
 
 end = struct
@@ -896,19 +889,19 @@ end = struct
   module TaskQueue = AsyncTaskQueue.Make(Task)
 
   let check_task_aux extra name l i =
-    let { r_stop; r_document; r_loc; r_name } = List.nth l i in
+    let { Stateid.stop; document; loc; name = r_name } = List.nth l i in
     Pp.msg_info(
       str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
-    VCS.restore r_document;
+    VCS.restore document;
     try
-      !Task.reach_known_state ~cache:`No r_stop;
+      !Task.reach_known_state ~cache:`No stop;
       (* The original terminator, a hook, has not been saved in the .vi*)
       Proof_global.set_terminator
         (Lemmas.standard_proof_terminator []
           (Lemmas.mk_hook (fun _ _ -> ())));
       let proof = Proof_global.close_proof (fun x -> x) in
-      vernac_interp r_stop ~proof
-        { verbose = false; loc = r_loc;
+      vernac_interp stop ~proof
+        { verbose = false; loc;
           expr = (VernacEndProof (Proved (true,None))) };
       Some proof
     with e ->
@@ -938,7 +931,7 @@ end = struct
                     str (Printexc.to_string e))); None
 
   let finish_task name (u,cst,_) d p l i =
-    let bucket = (List.nth l i).r_uuid in
+    let bucket = (List.nth l i).Stateid.uuid in
     match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with
     | None -> exit 1
     | Some (po,pt) ->
@@ -972,14 +965,14 @@ end = struct
     | None -> false
 
   let info_tasks l =
-    CList.map_i (fun i { r_loc; r_name } ->
+    CList.map_i (fun i { Stateid.loc; name } ->
       let time1 =
-        try float_of_string (Aux_file.get !hints r_loc "proof_build_time")
+        try float_of_string (Aux_file.get !hints loc "proof_build_time")
         with Not_found -> 0.0 in
       let time2 =
-        try float_of_string (Aux_file.get !hints r_loc "proof_check_time")
+        try float_of_string (Aux_file.get !hints loc "proof_check_time")
         with Not_found -> 0.0 in
-      r_name, max (time1 +. time2) 0.0001,i) 0 l
+      name, max (time1 +. time2) 0.0001,i) 0 l
 
   let set_perspective idl =
     let open Stateid in
@@ -1024,17 +1017,13 @@ end = struct
   let cancel_worker = TaskQueue.cancel_worker
 
   (* For external users this name is nicer than request *)
-  type tasks = int a_request list
-  let dump f2t_map =
-    let tasks = TaskQueue.dump () in
-    prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
-    List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map })
-      (CList.map_filter (Task.request_of_task `Fresh) tasks)
-  let dump_snapshot f2t_map =
+  type 'a tasks = ('a,VCS.vcs) Stateid.request list
+  let dump_snapshot () =
     let tasks = TaskQueue.snapshot () in
     prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
-    List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map })
-      (CList.map_filter (Task.request_of_task `Fresh) tasks)
+    CList.map_filter (Task.request_of_task `Fresh) tasks
+
+  let reset_task_queue () = TaskQueue.clear ()
 
 end
 
@@ -1236,7 +1225,8 @@ let collect_proof keep cur hd brkind id =
         else `Sync (name,proof_using_ast last,`Policy)
     | `Fork (_, hd', GuaranteesOpacity, ids) when
        has_proof_no_using last && not (State.is_cached (parent last)) &&
-       !Flags.compilation_mode = Flags.BuildVi ->
+       (!Flags.compilation_mode = Flags.BuildVi ||
+        !Flags.async_proofs_always_delegate) ->
         (try
           let name = name ids in
           let hint, time = get_hint_ctx loc, get_hint_bp_time name in
@@ -1602,8 +1592,9 @@ let join () =
   VCS.print ();
   VCS.print ()
 
-type tasks = Slaves.tasks * RemoteCounter.remote_counters_status
-let dump x = Slaves.dump x, RemoteCounter.backup ()
+let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot ()
+type document = VCS.vcs
+type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status
 let check_task name (tasks,rcbackup) i =
   RemoteCounter.restore rcbackup;
   let vcs = VCS.backup () in
@@ -1683,6 +1674,15 @@ let handle_failure e vcs tty =
       VCS.print ();
       raise e
 
+let snapshot_vi ldir long_f_dot_v =
+  finish ();
+  if List.length (VCS.branches ()) > 1 then
+    Errors.errorlabstrm "stm" (str"Cannot dump a vi with open proofs");
+  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
+    (Global.opaque_tables ())
+
+let reset_task_queue = Slaves.reset_task_queue
+
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
   let warn_if_pos a b =
     if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
diff --git a/stm/stm.mli b/stm/stm.mli
index d77c19cfb..c4664a67c 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -46,16 +46,25 @@ val stop_worker : string -> unit
 
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
-(* To save to disk an incomplete document *)
-type tasks
-val dump_final : int Future.UUIDMap.t -> tasks
-val dump_snapshot : int Future.UUIDMap.t -> tasks
 
+(* Saves on the dist a .vi corresponding to the current status:
+   - if the worker prool is empty, all tasks are saved
+   - if the worker proof is not empty, then it waits until all workers
+     are done with their current jobs and then dumps (or fails if one
+     of the completed tasks is a failuere) *)
+val snapshot_vi : DirPath.t -> string -> unit
+
+(* Empties the task queue, can be used only if the worker pool is empty (E.g.
+ * after having built a .vi in batch mode *)
+val reset_task_queue : unit -> unit
+
+(* A .vi contains tasks to be completed *)
+type tasks
 val check_task : string -> tasks -> int -> bool
 val info_tasks : tasks -> (string * float * int) list
 val finish_tasks : string ->
   Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
-  tasks -> Library.seg_univ * Library.seg_proofs
+    tasks -> Library.seg_univ * Library.seg_proofs
 
 (* Id of the tip of the current branch *)
 val get_current_state : unit -> Stateid.t
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index fe9cf015a..04e4e81f9 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -103,15 +103,6 @@ let wait_until_n_are_waiting_and_queue_empty j tq =
   done;
   Mutex.unlock tq.lock
 
-let dump { queue; lock } =
-  let l = ref [] in
-  Mutex.lock lock;
-  while not (PriorityQueue.is_empty queue) do
-    l := PriorityQueue.pop queue :: !l
-  done;
-  Mutex.unlock lock;
-  List.rev !l
-
 let wait_until_n_are_waiting_then_snapshot j tq =
   let l = ref [] in
   Mutex.lock tq.lock;
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index abb14f969..230ce032a 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -15,9 +15,6 @@ val push : 'a t -> 'a -> unit
 val set_order : 'a t -> ('a -> 'a -> int) -> unit
 val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
 
-(* also empties the queue *)
-val dump : 'a t -> 'a list
-
 (* Non destructive *)
 val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list