vi2vo: new flag -schedule-vi2vo

4 files changed, 61 insertions, 7 deletions

diff --git a/tools/coqc.ml b/tools/coqc.ml
index dbfdc40a2..e835091ea 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -151,7 +151,8 @@ 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 ->
+    | ("-schedule-vi-checking"
+      |"-check-vi-tasks" | "-schedule-vi2vo" as o) :: s :: rem ->
         let nodash, rem =
           CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in
         extra_arg_needed := false;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8a133fc48..d2f680d6e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -262,7 +262,7 @@ let check_vi_tasks () =
 
 let vi_files = ref []
 let vi_files_j = ref 0
-
+let vi_checking = ref false
 let add_vi_file f =
   set_batch_mode ();
   Flags.make_silent true;
@@ -273,7 +273,7 @@ let set_vi_checking_j opt j =
     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'";
+    prerr_endline "setting the J variable like in 'make vi2vo J=3'";
     exit 1
 
 let is_not_dash_option = function
@@ -281,8 +281,11 @@ let is_not_dash_option = function
   | _ -> false
 
 let schedule_vi_checking () =
-  if !vi_files <> [] then
+  if !vi_files <> [] && !vi_checking then
     Vi_checking.schedule_vi_checking !vi_files_j !vi_files
+let schedule_vi_compilation () =
+  if !vi_files <> [] && not !vi_checking then
+    Vi_checking.schedule_vi_compilation !vi_files_j !vi_files
 
 let parse_args arglist =
   let args = ref arglist in
@@ -323,6 +326,11 @@ let parse_args arglist =
         let tfile = next () in
         add_vi_task (tno,tfile)
     |"-schedule-vi-checking" ->
+        vi_checking := true;
+        set_vi_checking_j opt (next ());
+        add_vi_file (next ());
+        while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
+    |"-schedule-vi2vo" ->
         set_vi_checking_j opt (next ());
         add_vi_file (next ());
         while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
@@ -466,6 +474,7 @@ let init arglist =
       load_vernacular ();
       compile_files ();
       schedule_vi_checking ();
+      schedule_vi_compilation ();
       check_vi_tasks ();
       outputstate ()
     with any ->
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
index 5fae1c459..37f4266d0 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -105,3 +105,48 @@ let schedule_vi_checking j fs =
   done;
   exit !rc
 
+let schedule_vi_compilation 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 paths = Loadpath.get_paths () in
+    let _, long_f_dot_v =
+      System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+    let aux = Aux_file.load_aux_file_for long_f_dot_v in
+    let eta =
+      try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
+      with Not_found -> 0.0 in
+    jobs := (f, eta) :: !jobs)
+  fs;
+  let cmp_job (_,t1) (_,t2) = compare t2 t1 in
+  jobs := List.sort cmp_job !jobs;
+  let pool : Worker.process Pool.t ref = ref Pool.empty in
+  let rec filter_argv b = function
+    | [] -> []
+    | "-schedule-vi2vo" :: 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 prog = Sys.argv.(0) in  
+  let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
+  let make_job () =
+    let f, t = List.hd !jobs in
+    jobs := List.tl !jobs;
+    [ "-vi2vo"; f ] 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 21acbe294..65414eda4 100644
--- a/toplevel/vi_checking.mli
+++ b/toplevel/vi_checking.mli
@@ -8,7 +8,6 @@
 
 (* [check_vi tasks file] checks the [tasks] stored in [file] *)
 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] *)
 val schedule_vi_checking : int -> string list -> unit
+
+val schedule_vi_compilation : int -> string list -> unit