-schedule-vi-checking ported to spawn

8 files changed, 155 insertions, 76 deletions

diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 86bec7c21f..3dcd762aa2 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -124,8 +124,9 @@ The $coqtop -schedule-vi-checking 3 a b c$ command can be used to obtain
 a good scheduling for 3 workers to check all proof tasks of $a.vi$, $b.vi$ and
 $c.vi$.  Auxiliary files are used to predict how long a proof task will take,
 assuming it will take the same amount of time it took last time.
-The output of $coqtop -schedule-vi-checking$ is a list of commands one has
-to execute in order to check all proof tasks.
+If the $Makefile$ one uses was produced by $coq\_makefile$ the $checkproofs$
+target can be used to check all $.vi$ files.  The variable $J$ should be
+set to the number of workers, like in $make checkproofs J=3$.
 
 \subsubsection{Caveats}
 
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index eefad34421..ab4a89ffbf 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -616,7 +616,8 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     end;
   if !some_vfile then
     begin
-      print "quick:\n\t$(MAKE) all VO=vi\n";
+      print "quick:\n\t$(MAKE) -f $(firstword $(MAKEFILE_LIST)) all VO=vi\n";
+      print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vi-checking $(J) $(VOFILES:%.vo=%.vi)\n";
       print "gallina: $(GFILES)\n\n";
       print "html: $(GLOBFILES) $(VFILES)\n";
       print "\t- mkdir -p html\n";
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5e63322c5a..dbfdc40a2e 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -71,6 +71,7 @@ let usage () =
   exit 1
 
 (* parsing of the command line *)
+let extra_arg_needed = ref true
 
 let parse_args () =
   let rec parse (cfiles,args) = function
@@ -150,6 +151,11 @@ let parse_args () =
     | "-R" :: s :: "-as" :: t :: rem ->	parse (cfiles,t::"-as"::s::"-R"::args) rem
     | "-R" :: s :: "-as" :: [] -> usage ()
     | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
+    | ("-schedule-vi-checking" |"-check-vi-tasks" as o) :: s :: rem ->
+        let nodash, rem =
+          CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in
+        extra_arg_needed := false;
+        parse (cfiles, List.rev nodash @ s :: o :: args) rem
 
 (* Anything else is interpreted as a file *)
 
@@ -172,7 +178,7 @@ let parse_args () =
 
 let main () =
   let cfiles, args = parse_args () in
-    if cfiles = [] then begin
+    if cfiles = [] && !extra_arg_needed then begin
       prerr_endline "coqc: too few arguments" ;
       usage ()
     end;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 503e33cc51..74a94465e6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -254,7 +254,11 @@ let add_vi_task f =
   Flags.make_silent true;
   vi_tasks := f :: !vi_tasks
 
-let check_vi_tasks () = List.iter Vi_checking.check_vi (List.rev !vi_tasks)
+let check_vi_tasks () =
+  let rc =
+    List.fold_left (fun acc t -> Vi_checking.check_vi t && acc)
+      true (List.rev !vi_tasks) in
+  if not rc then exit 1
 
 let vi_files = ref []
 let vi_files_j = ref 0
@@ -263,7 +267,14 @@ let add_vi_file f =
   set_batch_mode ();
   Flags.make_silent true;
   vi_files := f :: !vi_files
-let set_vi_checking_j j = vi_files_j := int_of_string j
+let set_vi_checking_j opt j =
+  try vi_files_j := int_of_string j
+  with Failure _ ->
+    prerr_endline ("The first argument of " ^ opt ^ " must the number");
+    prerr_endline "of concurrent workers to be used (a positive integer).";
+    prerr_endline "Makefiles generated by coq_makefile should be called";
+    prerr_endline "setting the J variable like in 'make checkproofs J=3'";
+    exit 1
 
 let is_not_dash_option = function
   | Some f when String.length f > 0 && f.[0] <> '-' -> true
@@ -312,7 +323,7 @@ let parse_args arglist =
         let tfile = next () in
         add_vi_task (tno,tfile)
     |"-schedule-vi-checking" ->
-        set_vi_checking_j (next ());
+        set_vi_checking_j opt (next ());
         add_vi_file (next ());
         while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
 
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index ce1d6b1b9f..613ff672bf 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -583,15 +583,15 @@ let get_hint_ctx loc =
   let ids = List.map (fun id -> Loc.ghost, id) ids in
   SsExpr (SsSet ids)
 
-    module Worker = Spawn.Sync(struct 
-      let add_timeout ~sec f =
-        ignore(Thread.create (fun () ->
-          while true do
-            Unix.sleep sec;
-            if not (f ()) then Thread.exit ()
-          done)
-        ())
-    end)
+module Worker = Spawn.Sync(struct 
+  let add_timeout ~sec f =
+    ignore(Thread.create (fun () ->
+      while true do
+        Unix.sleep sec;
+        if not (f ()) then Thread.exit ()
+      done)
+    ())
+end)
 
 (* Slave processes (if initialized, otherwise local lazy evaluation) *)
 module Slaves : sig
@@ -617,7 +617,7 @@ module Slaves : sig
 
   type tasks
   val dump : unit -> tasks
-  val check_task : string -> tasks -> int -> unit
+  val check_task : string -> tasks -> int -> bool
   val info_tasks : tasks -> (string * float * int) list
 
 end = struct (* {{{ *)
@@ -800,16 +800,42 @@ end = struct (* {{{ *)
   let check_task name l i =
     match List.nth l i with
     | ReqBuildProof ((id,valid),eop,vcs,loc,s) ->
-        Pp.msg_info (str(Printf.sprintf "Checking task %d (%s) of %s" i s name));
+        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*)
-        Proof_global.set_terminator
-          (Lemmas.standard_proof_terminator [] (fun _ _ -> ()));
-        let proof = Proof_global.close_proof (fun x -> x) in
-        vernac_interp eop ~proof
-          { verbose = false; loc;
-            expr = (VernacEndProof (Proved (true,None))) }
+        try
+          !reach_known_state ~cache:`No eop;
+          (* The original terminator, a hook, has not been saved in the .vi*)
+          Proof_global.set_terminator
+            (Lemmas.standard_proof_terminator [] (fun _ _ -> ()));
+          let proof = Proof_global.close_proof (fun x -> x) in
+          vernac_interp eop ~proof
+            { verbose = false; loc;
+              expr = (VernacEndProof (Proved (true,None))) };
+          true
+        with e -> (try
+          match Stateid.get e with
+          | None ->
+              Pp.pperrnl Pp.(
+                str"File " ++ str name ++ str ": proof of " ++ str s ++
+                spc () ++ print e)
+          | Some (_, cur) ->
+              match VCS.visit cur with
+              | { step = `Cmd ( { loc }, _) } 
+              | { step = `Fork ( { loc }, _, _, _) } 
+              | { step = `Qed ( { qast = { loc } }, _) } 
+              | { step = `Sideff (`Ast ( { loc }, _)) } ->
+                  let start, stop = Loc.unloc loc in
+                  Pp.pperrnl Pp.(
+                    str"File " ++ str name ++ str ": proof of " ++ str s ++
+                    str ": chars " ++ int start ++ str "-" ++ int stop ++
+                    spc () ++ print e)
+              | _ ->
+                  Pp.pperrnl Pp.(
+                    str"File " ++ str name ++ str ": proof of " ++ str s ++
+                    spc () ++ print e)
+        with e ->
+          Pp.msg_error (str"unable to print error message: " ++
+                        str (Printexc.to_string e))); false
 
   let info_tasks l =
     CList.map_i (fun i (ReqBuildProof(_,_,_,loc,s)) ->
@@ -1159,6 +1185,8 @@ let string_of_reason = function
   | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity"
   | _ -> "Unknown Reason"
 
+let wall_clock_last_fork = ref 0.0
+
 let known_state ?(redefine_qed=false) ~cache id =
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
@@ -1168,8 +1196,6 @@ let known_state ?(redefine_qed=false) ~cache id =
     Lib.freeze ~marshallable:`No in
   let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
 
-  let wall_clock_last_fork = ref 0.0 in
-
   let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
     prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
     reach id;
@@ -1481,8 +1507,12 @@ type tasks = Slaves.tasks
 let dump () = Slaves.dump ()
 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
+  try
+    let rc = Future.purify (Slaves.check_task name tasks) i in
+    Pp.pperr_flush ();
+    VCS.restore vcs;
+    rc
+  with e when Errors.noncritical e -> VCS.restore vcs; false
 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 dddb7defe1..158f8820e6 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 : string -> tasks -> int -> unit
+val check_task : string -> tasks -> int -> bool
 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 fe76116242..a52a83dfe7 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -6,11 +6,30 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
+
 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 f tasks) ts
+  List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
+
+module Worker = Spawn.Sync(struct 
+  let add_timeout ~sec f =
+    ignore(Thread.create (fun () ->
+      while true do
+        Unix.sleep sec;
+        if not (f ()) then Thread.exit ()
+      done)
+    ())
+end)
+
+module IntOT = struct
+  type t = int
+  let compare = compare
+end
+
+module Pool = Map.Make(IntOT)
 
 let schedule_vi_checking j fs =
   if j < 1 then Errors.error "The number of workers must be bigger than 0";
@@ -22,31 +41,19 @@ let schedule_vi_checking j fs =
     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
-    jobs := List.map (fun (name,time,id) -> (f,id),name,time) infos @ !jobs)
-    fs;
-  let cmp_job (_,_,t1) (_,_,t2) = compare t2 t1 in
+    let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
+    if infos <> [] then jobs := (f, eta, infos) :: !jobs)
+  fs;
+  let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in
   jobs := List.sort cmp_job !jobs;
-  let workers = Array.make j (0.0,[]) in
-  let cmp_worker (t1,_) (t2,_) = compare t1 t2 in
-  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
-        let ((f,id),_,t as job) = List.hd !jobs in
-        let rest = List.tl !jobs in
-        let tot, joblist = workers.(i) in
-        workers.(i) <- tot +. t, job::joblist;
-        jobs := rest
-      done
-    done;
-  done;
-  for i=0 to j-1 do
-    let tot, joblist = workers.(i) in
-    let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
-    workers.(i) <- tot, List.sort cmp_job joblist
-  done;
+  let eta = ref (List.fold_left (fun a j -> a +. pi2 j) 0.0 !jobs) in
+  let pool : Worker.process Pool.t ref = ref Pool.empty in
+  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
   let pack = function
     | [] -> []
     | ((f,_),_,_) :: _ as l ->
@@ -55,23 +62,46 @@ 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
-  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"
+  let prog = Sys.argv.(0) in  
+  let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
+  let make_job () =
+    let cur = ref 0.0 in
+    let what = ref [] in
+    let j_left = j - Pool.cardinal !pool in
+    let take_next_file () =
+      let f, t, tasks = List.hd !jobs in
+      jobs := List.tl !jobs;
+      cur := !cur +. t;
+      what := (List.map (fun (n,t,id) -> (f,id),n,t) tasks) @ !what in
+    if List.length !jobs >= j_left then take_next_file ()
+    else while !jobs <> [] &&
+         !cur < max 0.0 (min 60.0 (!eta /. float_of_int j_left)) do
+      let f, t, tasks = List.hd !jobs in
+      jobs := List.tl !jobs;
+      let n, tt, id = List.hd tasks in
+      if List.length tasks > 1 then
+        jobs := (f, t -. tt, List.tl tasks) :: !jobs;
+      cur := !cur +. tt;
+      what := ((f,id),n,tt) :: !what;
+    done;
+    if !what = [] then take_next_file ();
+    eta := !eta -. !cur;
+    let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
+    List.flatten
+      (List.map (fun (f, tl) ->
+        "-check-vi-tasks" :: 
+        String.concat "," (List.map string_of_int tl) :: [f])
+      (pack (List.sort cmp_job !what))) in
+  let rc = ref 0 in
+  while !jobs <> [] || Pool.cardinal !pool > 0 do
+    while Pool.cardinal !pool < j && !jobs <> [] do
+      let args = Array.of_list (stdargs @ make_job ()) in
+      let proc, _, _ = Worker.spawn prog args in
+      pool := Pool.add (Worker.unixpid proc) proc !pool;
+    done;
+    let pid, ret = Unix.wait () in
+    if ret <> Unix.WEXITED 0 then rc := 1;
+    pool := Pool.remove pid !pool;
+  done;
+  exit !rc
 
diff --git a/toplevel/vi_checking.mli b/toplevel/vi_checking.mli
index 9866fdb973..21acbe294d 100644
--- a/toplevel/vi_checking.mli
+++ b/toplevel/vi_checking.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (* [check_vi tasks file] checks the [tasks] stored in [file] *)
-val check_vi : int list * string -> unit
+val check_vi : int list * string -> bool
 
 (* [schedule_vi_checking j files] prints [j] command lines to
  * be executed in parallel to check all tasks in [files] *)