-schedule-vi-checking generates better script

4 files changed, 38 insertions, 18 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b1d3e0cc24..840ba3e4cd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -267,7 +267,8 @@ let is_not_dash_option = function
   | _ -> false
 
 let schedule_vi_checking () =
-  Vi_checking.schedule_vi_checking !vi_files_j !vi_files
+  if !vi_files <> [] then
+    Vi_checking.schedule_vi_checking !vi_files_j !vi_files
 
 let parse_args arglist =
   let args = ref arglist in
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index fc888eea78..a0c5bcf2d9 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -607,7 +607,7 @@ module Slaves : sig
 
   type tasks
   val dump : unit -> tasks
-  val check_task : tasks -> int -> unit
+  val check_task : string -> tasks -> int -> unit
   val info_tasks : tasks -> (string * float * int) list
 
 end = struct (* {{{ *)
@@ -797,10 +797,10 @@ end = struct (* {{{ *)
         VCS.print ();
         r
 
-  let check_task l i =
+  let check_task name l i =
     match List.nth l i with
     | ReqBuildProof ((id,valid),eop,vcs,loc,s) ->
-        Pp.msg_info (str"Checking "++str s);
+        Pp.msg_info (str(Printf.sprintf "Checking task %d (%s) of %s" i s name));
         VCS.restore vcs;
         !reach_known_state ~cache:`No eop;
         (* The original terminator, a hook, has not been saved in the .vi*)
@@ -1498,7 +1498,10 @@ let join () =
 
 type tasks = Slaves.tasks
 let dump () = Slaves.dump ()
-let check_task tasks i = Slaves.check_task tasks i
+let check_task name tasks i =
+  let vcs = VCS.backup () in
+  try Future.purify (Slaves.check_task name tasks) i; VCS.restore vcs
+  with e when Errors.noncritical e -> VCS.restore vcs
 let info_tasks tasks = Slaves.info_tasks tasks
 
 let merge_proof_branch qast keep brname =
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 89efdc718f..dddb7defe1 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -44,7 +44,7 @@ val join : unit -> unit
 type tasks
 val dump : unit -> tasks
 
-val check_task : tasks -> int -> unit
+val check_task : string -> tasks -> int -> unit
 val info_tasks : tasks -> (string * float * int) list
 
 (* Id of the tip of the current branch *)
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
index debb1e9694..fe76116242 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -10,11 +10,15 @@ let check_vi (ts,f) =
   Dumpglob.noglob ();
   let tasks, long_f_dot_v = Library.load_library_todo f in
   Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
-  List.iter (Stm.check_task tasks) ts
+  List.iter (Stm.check_task f tasks) ts
 
 let schedule_vi_checking j fs =
+  if j < 1 then Errors.error "The number of workers must be bigger than 0";
   let jobs = ref [] in
   List.iter (fun f ->
+    let f =
+      if Filename.check_suffix f ".vi" then Filename.chop_extension f
+      else f in
     let tasks, long_f_dot_v = Library.load_library_todo f in
     Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
     let infos = Stm.info_tasks tasks in
@@ -24,7 +28,9 @@ let schedule_vi_checking j fs =
   jobs := List.sort cmp_job !jobs;
   let workers = Array.make j (0.0,[]) in
   let cmp_worker (t1,_) (t2,_) = compare t1 t2 in
-  while !jobs <> [] do
+  if j = 1 then
+     workers.(0) <- List.fold_left (fun acc (_,_,t) -> acc +. t) 0.0 !jobs, !jobs
+  else while !jobs <> [] do
     Array.sort cmp_worker workers;
     for i=0 to j-2 do
       while !jobs <> [] && fst workers.(i) <= fst workers.(i+1) do
@@ -49,13 +55,23 @@ let schedule_vi_checking j fs =
           | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl
           | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in
         aux f [] l in
-  Array.iter
-    (fun (tot, joblist) -> if joblist <> [] then
-       let joblist = pack joblist in
-       Printf.printf "%s -check-vi-tasks %s & # eta %.2f\n"
-         Sys.argv.(0)
-         (String.concat " -check-vi-tasks "
-           (List.map (fun (f,tl) ->
-              let tl = List.map string_of_int tl in
-              String.concat "," tl ^ " " ^ f) joblist)) tot)
-    workers
+  let prog =
+    let rec filter_argv b = function
+      | [] -> []
+      | "-schedule-vi-checking" :: rest -> filter_argv true rest
+      | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+      | _ :: rest when b -> filter_argv b rest
+      | s :: rest -> s :: filter_argv b rest in
+    String.concat " " (filter_argv false (Array.to_list Sys.argv)) in
+  Printf.printf "#!/bin/sh\n";
+  Array.iter (fun (tot, joblist) -> if joblist <> [] then
+    let joblist = pack joblist in
+    Printf.printf "( %s ) &\n"
+      (String.concat "; "
+        (List.map (fun tasks -> Printf.sprintf "%s -check-vi-tasks %s " prog tasks)
+          (List.map (fun (f,tl) ->
+             let tl = List.map string_of_int tl in
+             String.concat "," tl ^ " " ^ f) joblist))))
+    workers;
+  Printf.printf "wait\n"
+