coqtop: -check-vi-tasks and -schedule-vi-checking

The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2,
in this precise order, stored in a.vi.

The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi
and .{a,b,c}.aux and spits 4 command lines to check all the tasks in
{a,b,c}.vi trying to equally partition the job between the 4 workers,
that can indeed be run in parallel.
The aux file contains the time that it took to check the proofs stored
in the .vi files last time the file was fully checked.

This user interface is still very rough, it should probably run the
workers instead of just printing their command line.

10 files changed, 209 insertions, 39 deletions

diff --git a/library/library.ml b/library/library.ml
index 8b390832f..1088bcb16 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -394,6 +394,18 @@ let intern_from_file f =
   close_in ch;
   library
 
+let load_library_todo f =
+  let paths = Loadpath.get_paths () in
+  let _, longf =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let f = longf^"i" in
+  let ch = System.with_magic_number_check raw_intern_library f in
+  let _ = System.skip_in_segment f ch in
+  let tasks, _, _ = System.marshal_in_segment f ch in
+  match tasks with
+  | Some a -> a, longf
+  | None -> errorlabstrm "load_library_todo" (str"not a .vi file")
+
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
   try find_library dir, needed
diff --git a/library/library.mli b/library/library.mli
index 530209485..647138483 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -38,6 +38,7 @@ val start_library : string -> DirPath.t * string
 
 (** {6 End the compilation of a library and save it to a ".vo" file } *)
 val save_library_to : ?todo:'a -> DirPath.t -> string -> unit
+val load_library_todo : string -> 'a * string
 
 (** {6 Interrogate the status of libraries } *)
 
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 3b01f90c4..378f493ad 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -126,7 +126,8 @@ let parse_args () =
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
-      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem ->
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
+      |"-check-vi-tasks" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ad3ce7879..f902206e2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -238,6 +238,33 @@ let get_host_port opt s =
   | [host; port] -> Some (host, int_of_string port)
   | _ -> prerr_endline ("Error: host:port expected after option "^opt); exit 1
 
+let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
+
+let vi_tasks = ref []
+
+let add_vi_task f =
+  set_batch_mode ();
+  Flags.make_silent true;
+  vi_tasks := f :: !vi_tasks
+
+let check_vi_tasks () = List.iter Vi_checking.check_vi (List.rev !vi_tasks)
+
+let vi_files = ref []
+let vi_files_j = ref 0
+
+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 is_not_dash_option = function
+  | Some f when String.length f > 0 && f.[0] <> '-' -> true
+  | _ -> false
+
+let schedule_vi_checking () =
+  Vi_checking.schedule_vi_checking !vi_files_j !vi_files
+
 let parse_args arglist =
   let args = ref arglist in
   let extras = ref [] in
@@ -245,10 +272,14 @@ let parse_args arglist =
   | [] -> List.rev !extras
   | opt :: rem ->
     args := rem;
-    let next () = match rem with
+    let next () = match !args with
       | x::rem -> args := rem; x
       | [] -> error_missing_arg opt
     in
+    let peek_next () = match !args with
+      | x::_ -> Some x
+      | [] -> None
+    in
     begin match opt with
 
     (* Complex options with many args *)
@@ -266,6 +297,16 @@ let parse_args arglist =
       | d :: p :: rem -> set_rec_include d p; args := rem
       | _ -> error_missing_arg opt
       end
+    
+    (* Options with two arg *)
+    |"-check-vi-tasks" ->
+        let tno = get_task_list (next ()) in
+        let tfile = next () in
+        add_vi_task (tno,tfile)
+    |"-schedule-vi-checking" ->
+        set_vi_checking_j (next ());
+        add_vi_file (next ());
+        while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
 
     (* Options with one arg *)
     |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
@@ -396,6 +437,8 @@ let init arglist =
       load_rcfile();
       load_vernacular ();
       compile_files ();
+      schedule_vi_checking ();
+      check_vi_tasks ();
       outputstate ()
     with any ->
       flush_all();
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index f5cc9a856..bb531056f 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -571,12 +571,19 @@ end = struct (* {{{ *)
 end
 (* }}} *)
 
+let hints = ref Aux_file.empty_aux_file
+let set_compilation_hints h = hints := h
+let get_hint_ctx loc =
+  let s = Aux_file.get !hints loc "context_used" in
+  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+  let ids = List.map (fun id -> Loc.ghost, id) ids in
+  ids
 
 (* Slave processes (if initialized, otherwise local lazy evaluation) *)
 module Slaves : sig
 
   (* (eventually) remote calls *)
-  val build_proof :
+  val build_proof : loc:Loc.t ->
     exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t ->
       name:string -> future_proof * cancel_switch
 
@@ -596,6 +603,8 @@ module Slaves : sig
 
   type tasks
   val dump : unit -> tasks
+  val check_task : tasks -> int -> unit
+  val info_tasks : tasks -> (string * float * int) list
 
 end = struct (* {{{ *)
 
@@ -713,9 +722,10 @@ end = struct (* {{{ *)
   let set_reach_known_state f = reach_known_state := f
 
   type request =
-    ReqBuildProof of (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * string
+    ReqBuildProof of
+      (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * string
 
-  let name_of_request (ReqBuildProof (_,_,_,s)) = s
+  let name_of_request (ReqBuildProof (_,_,_,_,s)) = s
 
   type response =
     | RespBuiltProof of Entries.proof_output list 
@@ -741,33 +751,37 @@ end = struct (* {{{ *)
   type task =
     | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
         (Entries.proof_output list Future.assignement -> unit) * cancel_switch
-        * string
+        * Loc.t * string
   let pr_task = function
-    | TaskBuildProof(_,bop,eop,_,_,s) ->
+    | TaskBuildProof(_,bop,eop,_,_,_,s) ->
         "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^
           ","^s^")"
 
   let request_of_task task =
     match task with
-    | TaskBuildProof (exn_info,bop,eop,_,_,s) ->
-        ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,s)
+    | TaskBuildProof (exn_info,bop,eop,_,_,loc,s) ->
+        ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,s)
 
   let cancel_switch_of_task = function
-    | TaskBuildProof (_,_,_,_,c,_) -> c
+    | TaskBuildProof (_,_,_,_,c,_,_) -> c
 
-  let build_proof_here_core eop () =
+  let build_proof_here_core loc eop () =
+    let wall_clock1 = Unix.gettimeofday () in
     !reach_known_state ~cache:`No eop;
+    let wall_clock2 = Unix.gettimeofday () in
+    Aux_file.record_in_aux_at loc "proof_build_time"
+      (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
     Proof_global.return_proof ()
-  let build_proof_here (id,valid) eop =
-    Future.create (State.exn_on id ~valid) (build_proof_here_core eop)
+  let build_proof_here (id,valid) loc eop =
+    Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop)
 
   let slave_respond msg =
     match msg with
-    | ReqBuildProof(exn_info,eop,vcs,_) ->
+    | ReqBuildProof(exn_info,eop,vcs,loc,_) ->
         VCS.restore vcs;
         VCS.print ();
         let r = RespBuiltProof (
-          let l = Future.force (build_proof_here exn_info eop) in
+          let l = Future.force (build_proof_here exn_info loc eop) in
           List.iter (fun (_,se) -> Declareops.iter_side_effects (function
             | Declarations.SEsubproof(_,
                { Declarations.const_body = Declarations.OpaqueDef f;
@@ -779,6 +793,30 @@ end = struct (* {{{ *)
         VCS.print ();
         r
 
+  let check_task l i =
+    match List.nth l i with
+    | ReqBuildProof ((id,valid),eop,vcs,loc,s) ->
+        Pp.msg_info (str"Checking "++str s);
+        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))) }
+
+  let info_tasks l =
+    CList.map_i (fun i (ReqBuildProof(_,_,_,loc,s)) ->
+      let time1 =
+        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 loc "proof_check_time")
+        with Not_found -> 0.0 in
+      s,max (time1 +. time2) 0.0001,i) 0 l
+
   open Interface
 
   exception MarshalError of string
@@ -833,23 +871,23 @@ end = struct (* {{{ *)
       TQueue.wait_until_n_are_waiting_and_queue_empty
         (SlavesPool.n_slaves ()) queue
 
-  let build_proof ~exn_info:(id,valid as exn_info) ~start ~stop ~name =
+  let build_proof ~loc ~exn_info:(id,valid as exn_info) ~start ~stop ~name =
     let cancel_switch = ref false in
     if SlavesPool.is_empty () then
       if !Flags.compilation_mode = Flags.BuildVi then begin
         let force () : Entries.proof_output list Future.assignement =
-          try `Val (build_proof_here_core stop ()) with e -> `Exn e in
+          try `Val (build_proof_here_core loc stop ()) with e -> `Exn e in
         let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
         TQueue.push queue
-          (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,name));
+          (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
         f, cancel_switch
       end else
-        build_proof_here exn_info stop, cancel_switch
+        build_proof_here exn_info loc stop, cancel_switch
     else 
       let f, assign = Future.create_delegate (State.exn_on id ~valid) in
       Pp.feedback (Interface.InProgress 1);
       TQueue.push queue
-        (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,name));
+        (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
       f, cancel_switch
 
   exception RemoteException of std_ppcmds
@@ -882,13 +920,13 @@ end = struct (* {{{ *)
           let rec loop () =
             let response = unmarshal_response ic in
             match task, response with
-            | TaskBuildProof(_,_,_, assign,_,_), RespBuiltProof pl ->
+            | TaskBuildProof(_,_,_, assign,_,_,_), RespBuiltProof pl ->
                 assign (`Val pl);
                 (* We restart the slave, to avoid memory leaks.  We could just
                    Pp.feedback (Interface.InProgress ~-1) *)
                 last_task := None;
                 raise KillRespawn
-            | TaskBuildProof(_,_,_, assign,_,_), RespError (err_id,valid,e) ->
+            | TaskBuildProof(_,_,_, assign,_,_,_), RespError (err_id,valid,e) ->
                 let e = Stateid.add ~valid (RemoteException e) err_id in
                 assign (`Exn e);
                 (* We restart the slave, to avoid memory leaks.  We could just
@@ -920,8 +958,8 @@ end = struct (* {{{ *)
             msg_warning(strbrk("Marshalling error: "^s^". "^
               "The system state could not be sent to the slave process. "^
               "Falling back to local, lazy, evaluation."));
-            let TaskBuildProof (exn_info, _, stop, assign,_,_) = task in
-            assign(`Comp(build_proof_here exn_info stop));
+            let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+            assign(`Comp(build_proof_here exn_info loc stop));
             Pp.feedback (Interface.InProgress ~-1)
         | (Sys_error _ | Invalid_argument _ | End_of_file | KillRespawn) as e ->
             raise e (* we pass the exception to the external handler *)
@@ -949,8 +987,8 @@ end = struct (* {{{ *)
         (match !last_task with
         | Some task ->
             msg_warning(strbrk "Falling back to local, lazy, evaluation.");
-            let TaskBuildProof (exn_info, _, stop, assign,_,_) = task in
-            assign(`Comp(build_proof_here exn_info stop));
+            let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+            assign(`Comp(build_proof_here exn_info loc stop));
             Pp.feedback (Interface.InProgress ~-1);
         | None -> ());
         close_in ic;
@@ -1055,14 +1093,6 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
-let hints = ref Aux_file.empty_aux_file
-let set_compilation_hints h = hints := h
-let get_hint_ctx loc =
-  let s = Aux_file.get !hints loc "context_used" in
-  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
-  let ids = List.map (fun id -> Loc.ghost, id) ids in
-  ids
-
 (* Runs all transactions needed to reach a state *)
 module Reach : sig
 
@@ -1181,17 +1211,17 @@ let known_state ?(redefine_qed=false) ~cache id =
                 | VtKeep, { VCS.kind = `Edit _ }, Some (ofp, cancel) ->
                     assert(redefine_qed = true);
                     VCS.create_cluster nodes ~tip:id;
-                    let fp, cancel =
-                      Slaves.build_proof ~exn_info:(id,eop) ~start ~stop:eop
+                    let fp, cancel = Slaves.build_proof
+                        ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop
                         ~name:(String.concat " " (List.map Id.to_string ids)) in
                     Future.replace ofp fp;
                     qed.fproof <- Some (fp, cancel)
                 | VtKeep, { VCS.kind = `Proof _ }, Some _ -> assert false
                 | VtKeep, { VCS.kind = `Proof _ }, None ->
                     reach ~cache:`Shallow start;
-                    let fp, cancel =
-                      Slaves.build_proof ~exn_info:(id,eop) ~start ~stop:eop
-                        ~name:(String.concat " " (List.map Id.to_string ids)) in
+                    let fp, cancel = Slaves.build_proof
+                      ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop
+                      ~name:(String.concat " " (List.map Id.to_string ids)) in
                     qed.fproof <- Some (fp, cancel);
                     let proof =
                       Proof_global.close_future_proof ~feedback_id:id fp in
@@ -1459,6 +1489,8 @@ let join () =
 
 type tasks = Slaves.tasks
 let dump () = Slaves.dump ()
+let check_task tasks i = Slaves.check_task tasks i
+let info_tasks tasks = Slaves.info_tasks tasks
 
 let merge_proof_branch qast keep brname =
   let brinfo = VCS.get_branch brname in
@@ -1917,6 +1949,7 @@ let show_script ?proof () =
     let indented_cmds = List.rev (indented_cmds) in
     msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds))
   with Proof_global.NoCurrentProof -> ()
+  | Vcs_aux.Expired -> ()
 
 let () = Vernacentries.show_script := show_script
 
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 4949845b5..89efdc718 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -44,6 +44,9 @@ val join : unit -> unit
 type tasks
 val dump : unit -> tasks
 
+val check_task : tasks -> int -> unit
+val info_tasks : tasks -> (string * float * int) list
+
 (* Id of the tip of the current branch *)
 val get_current_state : unit -> Stateid.t
 
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 0ad82abd3..6f39725ff 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -23,4 +23,5 @@ Ide_slave
 Usage
 Coqloop
 Coqinit
+Vi_checking
 Coqtop
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 789f6bebb..d9c23c0ad 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -371,3 +371,4 @@ let compile verbosely f =
       check_pending_proofs ();
       let todo = Stm.dump () in
       Library.save_library_to ~todo ldir long_f_dot_v
+
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
new file mode 100644
index 000000000..debb1e969
--- /dev/null
+++ b/toplevel/vi_checking.ml
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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
+
+let schedule_vi_checking j fs =
+  let jobs = ref [] in
+  List.iter (fun f ->
+    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
+  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
+    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 pack = function
+    | [] -> []
+    | ((f,_),_,_) :: _ as l ->
+        let rec aux last acc = function
+          | [] -> [last,acc]
+          | ((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
diff --git a/toplevel/vi_checking.mli b/toplevel/vi_checking.mli
new file mode 100644
index 000000000..9866fdb97
--- /dev/null
+++ b/toplevel/vi_checking.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* [check_vi tasks file] checks the [tasks] stored in [file] *)
+val check_vi : int list * string -> unit
+
+(* [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