Stm: smarter delegation policy

Stm used to delegate every proof when it was possible, but this may
be a bad idea.  Small proofs may take less time than the overhead
delegation implies (marshalling, etc...).

Now it delegates only proofs that take >= 1 second.

By default a proof takes 1 second (that may be wrong).

If the file was compiled before, it reuses the data stored in the .aux
file and assumes the timings are still valid.

After a proof is checked, Coq knows how long it takes for real, so it
wont predict it wrong again (when the user goes up and down in the
file for example).

CoqIDE now sends to Coq, as part of the init message, the file name
so that Coq can load the .aux file.

5 files changed, 98 insertions, 58 deletions

diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 1b97a69ba..8ea5de365 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -233,9 +233,6 @@ let hints () =
 
 (** Other API calls *)
 
-let inloadpath dir =
-  Loadpath.is_in_load_paths (CUnix.physical_path_of_string dir)
-
 let status force =
   (** We remove the initial part of the current [DirPath.t]
       (usually Top in an interactive session, cf "coqtop -top"),
@@ -301,9 +298,23 @@ let handle_exn e =
 
 let init =
   let initialized = ref false in
-  fun () ->
+  fun file ->
    if !initialized then anomaly (str "Already initialized")
-   else (initialized := true; Stm.get_current_state ())
+   else begin
+     initialized := true;
+     match file with
+     | None -> Stm.get_current_state ()
+     | Some file ->
+         let dir = Filename.dirname file in
+         let open Loadpath in let open CUnix in
+         let initial_id, _ =
+           if not (is_in_load_paths (physical_path_of_string dir)) then
+             Stm.add false ~ontop:(Stm.get_current_state ())
+               0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
+           else Stm.get_current_state (), `NewTip in
+         Stm.set_compilation_hints file;
+         initial_id
+   end
 
 (* Retrocompatibility stuff *)
 let interp ((_raw, verbose), s) =
@@ -344,7 +355,6 @@ let eval_call xml_oc log c =
     Interface.hints = interruptible hints;
     Interface.status = interruptible status;
     Interface.search = interruptible search;
-    Interface.inloadpath = interruptible inloadpath;
     Interface.get_options = interruptible get_options;
     Interface.set_options = interruptible set_options;
     Interface.mkcases = interruptible Vernacentries.make_cases;
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 9cb5e9511..c61258655 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -502,8 +502,8 @@ module State : sig
   val install_cached : Stateid.t -> unit
   val is_cached : Stateid.t -> bool
 
-  val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn
 
+  val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn
   (* to send states across worker/master *)
   type frozen_state
   val get_cached : Stateid.t -> frozen_state
@@ -595,13 +595,18 @@ end
 (* }}} *)
 
 let hints = ref Aux_file.empty_aux_file
-let set_compilation_hints h = hints := h
+let set_compilation_hints file =
+  hints := Aux_file.load_aux_file_for file
 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
   SsExpr (SsSet ids)
 
+let get_hint_bp_time proof_name =
+  try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
+  with Not_found -> 1.0
+
 module Worker = Spawn.Sync(struct 
   let add_timeout ~sec f =
     ignore(Thread.create (fun () ->
@@ -612,6 +617,14 @@ module Worker = Spawn.Sync(struct
     ())
 end)
 
+let record_pb_time proof_name loc time =
+  let proof_build_time = Printf.sprintf "%.3f" time in
+  Aux_file.record_in_aux_at loc "proof_build_time" proof_build_time;
+  if proof_name <> "" then begin
+    Aux_file.record_in_aux_at Loc.ghost proof_name proof_build_time;
+    hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
+  end
+
 (* Slave processes (if initialized, otherwise local lazy evaluation) *)
 module Slaves : sig
 
@@ -773,7 +786,7 @@ end = struct (* {{{ *)
   let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s
 
   type response =
-    | RespBuiltProof of Entries.proof_output list 
+    | RespBuiltProof of Entries.proof_output list * float
     | RespError of (* err, safe, msg, safe_state *)
         Stateid.t * Stateid.t * std_ppcmds * State.frozen_state option
     | RespFeedback of Interface.feedback
@@ -825,7 +838,8 @@ end = struct (* {{{ *)
     | ReqBuildProof(exn_info,eop,vcs,loc,_,_) ->
         VCS.restore vcs;
         VCS.print ();
-        let r = RespBuiltProof (
+        let rc, time =
+          let wall_clock = Unix.gettimeofday () in
           let l = Future.force (build_proof_here exn_info loc eop) in
           List.iter (fun (_,se) -> Declareops.iter_side_effects (function
             | Declarations.SEsubproof(_,
@@ -833,9 +847,9 @@ end = struct (* {{{ *)
                Opaqueproof.join_opaque f
             | _ -> ())
           se) l;
-          l) in
+          l, Unix.gettimeofday () -. wall_clock in
         VCS.print ();
-        r
+        RespBuiltProof(rc,time)
 
   let check_task_aux extra name l i =
     match List.nth l i with
@@ -974,8 +988,8 @@ end = struct (* {{{ *)
           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
         let uuid = Future.uuid f in
-        TQueue.push queue
-          (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
+        TQueue.push queue (TaskBuildProof
+          (exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
         f, cancel_switch
       end else
         build_proof_here exn_info loc stop, cancel_switch
@@ -983,8 +997,8 @@ end = struct (* {{{ *)
       let f, assign = Future.create_delegate (State.exn_on id ~valid) in
       let uuid = Future.uuid f in
       Pp.feedback (Interface.InProgress 1);
-      TQueue.push queue
-        (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
+      TQueue.push queue (TaskBuildProof
+        (exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
       f, cancel_switch
 
   exception RemoteException of std_ppcmds
@@ -1028,13 +1042,16 @@ end = struct (* {{{ *)
           let rec loop () =
             let response = unmarshal_response ic in
             match task, response with
-            | TaskBuildProof(_,_,_, assign,_,_,_,_), RespBuiltProof pl ->
+            | TaskBuildProof(_,_,_, assign,_,loc,_,s),
+              RespBuiltProof(pl, time)->
                 assign (`Val pl);
                 (* We restart the slave, to avoid memory leaks.  We could just
                    Pp.feedback (Interface.InProgress ~-1) *)
+                record_pb_time s loc time;
                 last_task := None;
                 raise KillRespawn
-            | TaskBuildProof(_,_,_, assign,_,_,_,_),RespError(err_id,valid,e,s) ->
+            | TaskBuildProof(_,_,_, assign,_,_,_,_),
+              RespError(err_id,valid,e,s) ->
                 let e = Stateid.add ~valid (RemoteException e) err_id in
                 assign (`Exn e);
                 Option.iter (State.assign valid) s;
@@ -1216,15 +1233,19 @@ end = struct (* {{{ *)
 
 let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 
-let delegate_policy_check () =
+let delegate_policy_check time =
   if interactive () = `Yes then
-    !Flags.async_proofs_mode = Flags.APonParallel 0 ||
-    !Flags.async_proofs_mode = Flags.APonLazy
+    (!Flags.async_proofs_mode = Flags.APonParallel 0 ||
+    !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0
   else if !Flags.compilation_mode = Flags.BuildVi then true
   else !Flags.async_proofs_mode <> Flags.APoff
 
 let collect_proof cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
+ let no_name = "" in
+ let name = function
+   | [] -> no_name
+   | id :: _ -> Id.to_string id in
  let loc = (snd cur).loc in
  let is_defined = function
    | _, { expr = VernacEndProof (Proved (false,_)) } -> true
@@ -1233,40 +1254,54 @@ let collect_proof cur hd brkind id =
     let view = VCS.visit id in
     match last, view.step with
     | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
-    | _, `Alias _ -> `Sync `Alias
-    | _, `Fork(_,_,_,_::_::_)-> `Sync `MutualProofs
+    | _, `Alias _ -> `Sync (no_name,`Alias)
+    | _, `Fork(_,_,_,_::_::_)-> `Sync (no_name,`MutualProofs)
     | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) ->
-        `Sync `Doesn'tGuaranteeOpacity
+        `Sync (no_name,`Doesn'tGuaranteeOpacity)
     | Some (parent, ({ expr = VernacProof(_,Some _)} as v)),
       `Fork (_, hd', GuaranteesOpacity, ids) ->
+        let name = name ids in
+        let time = get_hint_bp_time name in
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
-        if delegate_policy_check () then `ASync (parent,Some v,accn,ids)
-        else `Sync `Policy
+        if delegate_policy_check time
+        then `ASync (parent,Some v,accn,name)
+        else `Sync (name,`Policy)
     | Some (parent, ({ expr = VernacProof(t,None)} as v)),
       `Fork (_, hd', GuaranteesOpacity, ids) when
        not (State.is_cached parent) &&
        !Flags.compilation_mode = Flags.BuildVi ->
         (try
-          let hint = get_hint_ctx loc in
+          let name = name ids in
+          let hint, time = get_hint_ctx loc, get_hint_bp_time name in
           assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
           v.expr <- VernacProof(t, Some hint);
-          if delegate_policy_check () then `ASync (parent,Some v,accn,ids)
-          else `Sync `Policy
-        with Not_found -> `Sync `NoHint)
+          if delegate_policy_check time
+          then `ASync (parent,Some v,accn,name)
+          else `Sync (name,`Policy)
+        with Not_found -> `Sync (no_name,`NoHint))
     | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
-        if delegate_policy_check () then `MaybeASync (parent, accn, ids)
-        else `Sync `Policy
-    | _, `Sideff _ -> `Sync `NestedProof
-    | _ -> `Sync `Unknown in
+        let name = name ids in
+        let time = get_hint_bp_time name in
+        if delegate_policy_check time
+        then `MaybeASync (parent, accn, name)
+        else `Sync (name,`Policy)
+    | _, `Sideff _ -> `Sync (no_name,`NestedProof)
+    | _ -> `Sync (no_name,`Unknown) in
  match cur, (VCS.visit id).step, brkind with
  |( parent, { expr = VernacExactProof _ }), `Fork _, _ ->
-     `Sync `Immediate
+     `Sync (no_name,`Immediate)
  | _, _, { VCS.kind = `Edit _ }  -> collect (Some cur) [] id
  | _ ->
-     if State.is_cached id then `Sync `AlreadyEvaluated
-     else if is_defined cur then `Sync `Transparent
-     else collect (Some cur) [] id
+     if is_defined cur then `Sync (no_name,`Transparent)
+     else
+       let rc = collect (Some cur) [] id in
+       if not (State.is_cached id) then rc
+       else (* we already have the proof, no gain in delaying *)
+         match rc with
+         | `Sync(name,_) -> `Sync (name,`AlreadyEvaluated)
+         | `MaybeASync(_,_,name) -> `Sync (name,`AlreadyEvaluated)
+         | `ASync(_,_,_,name) -> `Sync (name,`AlreadyEvaluated)
 
 let string_of_reason = function
   | `Transparent -> "Transparent"
@@ -1318,7 +1353,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), `Yes
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
           let rec aux = function
-          | `ASync (start, proof_using_ast, nodes,ids) -> (fun () ->
+          | `ASync (start, proof_using_ast, nodes, name) -> (fun () ->
                 prerr_endline ("Asynchronous " ^ Stateid.to_string id);
                 VCS.create_cluster nodes ~tip:id;
                 begin match keep, brinfo, qed.fproof with
@@ -1327,16 +1362,14 @@ let known_state ?(redefine_qed=false) ~cache id =
                     assert(redefine_qed = true);
                     VCS.create_cluster nodes ~tip:id;
                     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
+                      ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name 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
-                      ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop
-                      ~name:(String.concat " " (List.map Id.to_string ids)) in
+                      ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in
                     qed.fproof <- Some (fp, cancel);
                     let proof =
                       Proof_global.close_future_proof ~feedback_id:id fp in
@@ -1351,17 +1384,16 @@ let known_state ?(redefine_qed=false) ~cache id =
                 end;
                 Proof_global.discard_all ()
               ), if redefine_qed then `No else `Yes
-          | `Sync `Immediate -> (fun () -> 
+          | `Sync (name, `Immediate) -> (fun () -> 
                 assert (Stateid.equal view.next eop);
                 reach eop; vernac_interp id x; Proof_global.discard_all ()
               ), `Yes
-          | `Sync reason -> (fun () ->
+          | `Sync (name, reason) -> (fun () ->
                 prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^
                   string_of_reason reason);
                 reach eop;
                 let wall_clock = Unix.gettimeofday () in
-                Aux_file.record_in_aux_at x.loc "proof_build_time"
-                  (Printf.sprintf "%.3f" (wall_clock -. !wall_clock_last_fork));
+                record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork);
                 begin match keep with
                 | VtKeep ->
                     let proof =
@@ -1378,16 +1410,13 @@ let known_state ?(redefine_qed=false) ~cache id =
                 end;
                 Proof_global.discard_all ()
               ), `Yes
-          | `MaybeASync (start, nodes, ids) -> (fun () ->
+          | `MaybeASync (start, nodes, name) -> (fun () ->
                 prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id);
                 reach ~cache:`Shallow start;
                 (* no sections *)
                 if List.is_empty (Environ.named_context (Global.env ()))
-                   (* && Safe_typing.is_curmod_library (Global.safe_env ()) *)
-                then
-                  fst (aux (`ASync (start, None, nodes,ids))) ()
-                else
-                  fst (aux (`Sync `Unknown)) ()
+                then fst (aux (`ASync (start, None, nodes, name))) ()
+                else fst (aux (`Sync (name, `Unknown))) ()
               ), if redefine_qed then `No else `Yes
           in
           aux (collect_proof (view.next, x) brname brinfo eop)
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 1eba274ab..cd9245895 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -60,7 +60,8 @@ val init : unit -> unit
 val slave_main_loop : unit -> unit
 val slave_init_stdout : unit -> unit
 
-val set_compilation_hints : Aux_file.aux_file -> unit
+(* Filename *)
+val set_compilation_hints : string -> unit
 
 (** read-eval-print loop compatible interface ****************************** **)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 11cb726c7..27509fcc0 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -336,7 +336,7 @@ let compile verbosely f =
   | BuildVi ->
       let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
       Dumpglob.noglob ();
-      Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+      Stm.set_compilation_hints long_f_dot_v;
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
@@ -347,7 +347,7 @@ let compile verbosely f =
       Dumpglob.noglob ();
       let f = if check_suffix f ".vi" then chop_extension f else f in
       let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
-      Stm.set_compilation_hints (Aux_file.load_aux_file_for lfdv);
+      Stm.set_compilation_hints lfdv;
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv lib univs proofs
 
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
index 37f4266d0..cb6e60136 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -11,7 +11,7 @@ open Util
 let check_vi (ts,f) =
   Dumpglob.noglob ();
   let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
-  Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+  Stm.set_compilation_hints long_f_dot_v;
   List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
 
 module Worker = Spawn.Sync(struct 
@@ -39,7 +39,7 @@ let schedule_vi_checking j fs =
       if Filename.check_suffix f ".vi" then Filename.chop_extension f
       else f in
     let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
-    Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+    Stm.set_compilation_hints long_f_dot_v;
     let infos = Stm.info_tasks tasks in
     let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
     if infos <> [] then jobs := (f, eta, infos) :: !jobs)