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.

13 files changed, 130 insertions, 125 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 280f1df68e..3dd2ce0065 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -511,7 +511,6 @@ let eval_call ?(logger=default_logger) call handle k =
 let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x)
 let edit_at i = eval_call (Serialize.edit_at i)
 let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x)
-let inloadpath s = eval_call (Serialize.inloadpath s)
 let mkcases s = eval_call (Serialize.mkcases s)
 let status ?logger force = eval_call ?logger (Serialize.status force)
 let hints x = eval_call (Serialize.hints x)
diff --git a/ide/coq.mli b/ide/coq.mli
index 0b246b8420..542cc44620 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -126,7 +126,6 @@ val goals      : ?logger:Ideutils.logger ->
                  Interface.goals_sty      -> Interface.goals_rty query
 val evars      : Interface.evars_sty      -> Interface.evars_rty query
 val hints      : Interface.hints_sty      -> Interface.hints_rty query
-val inloadpath : Interface.inloadpath_sty -> Interface.inloadpath_rty query
 val mkcases    : Interface.mkcases_sty    -> Interface.mkcases_rty query
 val search     : Interface.search_sty     -> Interface.search_rty query
 val init       : Interface.init_sty       -> Interface.init_rty query
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index a43a7989a1..18069c471b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -764,32 +764,7 @@ object(self)
       let next = function
       | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return ()
       | Good id -> initial_state <- id; Coq.return () in
-      Coq.bind (Coq.init ()) next in
-    let add_load_path = match get_filename () with
-    | None -> Coq.return ()
-    | Some f ->
-      let dir = Filename.dirname f in
-      let loadpath = Coq.inloadpath dir in
-      let next = function
-      | Fail (_, _, s) ->
-        messages#set
-          ("Could not determine lodpath, this might lead to problems:\n"^s);
-        Coq.return ()
-      | Good true -> Coq.return ()
-      | Good false ->
-        let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-        let cmd = Coq.add ((cmd,hidden_edit_id ()),(Stateid.initial,false)) in
-        let next = function
-        | Fail (_, l, str) ->
-          messages#set ("Couln't add loadpath:\n"^str);
-          Coq.return ()
-        | Good (id, _) ->
-          initial_state <- id; Coq.return ()
-        in
-        Coq.bind cmd next
-      in
-      Coq.bind loadpath next
-    in
-    Coq.seq get_initial_state (Coq.seq add_load_path Coq.PrintOpt.enforce)
+      Coq.bind (Coq.init (get_filename ())) next in
+    Coq.seq get_initial_state Coq.PrintOpt.enforce
 
 end
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index 5a3d297468..80ac14f7d0 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -20,10 +20,16 @@ let oc = ref None
 let aux_file_name_for vfile =
   dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux"
 
+let mk_absolute vfile =
+  let vfile = CUnix.remove_path_dot vfile in
+  if Filename.is_relative vfile then CUnix.correct_path vfile (Sys.getcwd ())
+  else vfile
+
 let start_aux_file_for vfile =
+  let vfile = mk_absolute vfile in
   oc := Some (open_out (aux_file_name_for vfile));
   Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n"
-    version (Digest.to_hex (Digest.file vfile)) (CUnix.strip_path vfile)
+    version (Digest.to_hex (Digest.file vfile)) vfile
 
 let stop_aux_file () =
   close_out (Option.get !oc);
@@ -52,33 +58,35 @@ let record_in_aux_set_at loc = current_loc := loc
 
 let record_in_aux key v = record_in_aux_at !current_loc key v
 
-exception Outdated
+let set h loc k v =
+  let m = try H.find loc h with Not_found -> M.empty in
+  H.add loc (M.add k v m) h
 
 let load_aux_file_for vfile =
+  let vfile = mk_absolute vfile in
   let ret3 x y z = x, y, z in
   let ret4 x y z t = x, y, z, t in
   let h = ref empty_aux_file in
-  let add loc k v =
-    let m = try H.find loc !h with Not_found -> M.empty in
-    h := H.add loc (M.add k v m) !h in
+  let add loc k v = h := set !h loc k v in
   let aux_fname = aux_file_name_for vfile in
   try
     let ic = open_in aux_fname in
     let ver, hash, fname = Scanf.fscanf ic "COQAUX%d %s %s\n" ret3 in
     if ver <> version then raise (Failure "aux file version mismatch");
-    if fname <> CUnix.strip_path vfile then
+    if fname <> vfile then
       raise (Failure "aux file name mismatch");
-    if Digest.to_hex (Digest.file vfile) <> hash then raise Outdated;
+    let only_dummyloc = Digest.to_hex (Digest.file vfile) <> hash in
     while true do
       let i, j, k, v = Scanf.fscanf ic "%d %d %s %S\n" ret4 in
-      add (i,j) k v;
+      if not only_dummyloc || (i = 0 && j = 0) then add (i,j) k v;
     done;
     raise End_of_file
   with
   | End_of_file -> !h
-  | Outdated -> empty_aux_file
   | Sys_error s | Scanf.Scan_failure s
   | Failure s | Invalid_argument s ->
      Flags.if_verbose
        Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
      empty_aux_file
+
+let set h loc k v = set h (Loc.unloc loc) k v
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index b24515c993..f31b234083 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -11,6 +11,7 @@ type aux_file
 val load_aux_file_for : string -> aux_file
 val get : aux_file -> Loc.t -> string -> string
 val empty_aux_file : aux_file
+val set : aux_file -> Loc.t -> string -> string -> aux_file
 
 val start_aux_file_for : string -> unit
 val stop_aux_file : unit -> unit 
diff --git a/lib/interface.mli b/lib/interface.mli
index a089eb574c..8af26196c4 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -212,10 +212,6 @@ type get_options_rty = (option_name * option_state) list
 type set_options_sty = (option_name * option_value) list
 type set_options_rty = unit
 
-(** Is a directory part of Coq's loadpath ? *)
-type inloadpath_sty = string
-type inloadpath_rty = bool
-
 (** Create a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
     followed by enough pattern variables. *)
@@ -226,8 +222,10 @@ type mkcases_rty = string list list
 type quit_sty = unit
 type quit_rty = unit
 
-(* Initialize, and return the initial state id *)
-type init_sty = unit
+(* Initialize, and return the initial state id.  The argument is the filename.
+ * If its directory is not in dirpath, it adds it.  It also loads
+ * compilation hints for the filename. *)
+type init_sty = string option
 type init_rty = state_id
 
 type about_sty = unit
@@ -256,7 +254,6 @@ type handler = {
   search      : search_sty      -> search_rty;
   get_options : get_options_sty -> get_options_rty;
   set_options : set_options_sty -> set_options_rty;
-  inloadpath  : inloadpath_sty  -> inloadpath_rty;
   mkcases     : mkcases_sty     -> mkcases_rty;
   about       : about_sty       -> about_rty;
   stop_worker : stop_worker_sty -> stop_worker_rty;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 386ab8e45a..d91f736fd9 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20130918"
+let protocol_version = "20140312"
 
 (** * Interface of calls to Coq by CoqIde *)
 
@@ -617,11 +617,10 @@ let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t)
 let get_options_sty_t : get_options_sty val_t = unit_t
 let set_options_sty_t : set_options_sty val_t =
   list_t (pair_t (list_t string_t) option_value_t)
-let inloadpath_sty_t : inloadpath_sty val_t = string_t
 let mkcases_sty_t : mkcases_sty val_t = string_t
 let quit_sty_t : quit_sty val_t = unit_t
 let about_sty_t : about_sty val_t = unit_t
-let init_sty_t : init_sty val_t = unit_t
+let init_sty_t : init_sty val_t = option_t string_t
 let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
 let stop_worker_sty_t : stop_worker_sty val_t = int_t
 
@@ -640,7 +639,6 @@ let search_rty_t : search_rty val_t = list_t (coq_object_t string_t)
 let get_options_rty_t : get_options_rty val_t =
   list_t (pair_t (list_t string_t) option_state_t) 
 let set_options_rty_t : set_options_rty val_t = unit_t
-let inloadpath_rty_t : inloadpath_rty val_t = bool_t
 let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t)
 let quit_rty_t : quit_rty val_t = unit_t
 let about_rty_t : about_rty val_t = coq_info_t
@@ -660,7 +658,6 @@ let calls = [|
   "Search",     ($)search_sty_t,      ($)search_rty_t;
   "GetOptions", ($)get_options_sty_t, ($)get_options_rty_t;
   "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t;
-  "InLoadPath", ($)inloadpath_sty_t,  ($)inloadpath_rty_t;
   "MkCases",    ($)mkcases_sty_t,     ($)mkcases_rty_t;
   "Quit",       ($)quit_sty_t,        ($)quit_rty_t;
   "About",      ($)about_sty_t,       ($)about_rty_t;
@@ -680,7 +677,6 @@ type 'a call =
   | Search     of search_sty
   | GetOptions of get_options_sty
   | SetOptions of set_options_sty
-  | InLoadPath of inloadpath_sty
   | MkCases    of mkcases_sty
   | Quit       of quit_sty
   | About      of about_sty
@@ -700,13 +696,12 @@ let id_of_call = function
   | Search _     -> 7
   | GetOptions _ -> 8
   | SetOptions _ -> 9
-  | InLoadPath _ -> 10
-  | MkCases _    -> 11
-  | Quit _       -> 12
-  | About _      -> 13
-  | Init _       -> 14
-  | Interp _     -> 15
-  | StopWorker _ -> 16
+  | MkCases _    -> 10
+  | Quit _       -> 11
+  | About _      -> 12
+  | Init _       -> 13
+  | Interp _     -> 14
+  | StopWorker _ -> 15
 
 let str_of_call c = pi1 calls.(id_of_call c)
 
@@ -722,7 +717,6 @@ let hints x       : hints_rty call       = Hints x
 let status x      : status_rty call      = Status x
 let get_options x : get_options_rty call = GetOptions x
 let set_options x : set_options_rty call = SetOptions x
-let inloadpath x  : inloadpath_rty call  = InLoadPath x
 let mkcases x     : mkcases_rty call     = MkCases x
 let search x      : search_rty call      = Search x
 let quit x        : quit_rty call        = Quit x
@@ -744,7 +738,6 @@ let abstract_eval_call handler (c : 'a call) : 'a value =
     | Search x     -> mkGood (handler.search x)
     | GetOptions x -> mkGood (handler.get_options x)
     | SetOptions x -> mkGood (handler.set_options x)
-    | InLoadPath x -> mkGood (handler.inloadpath x)
     | MkCases x    -> mkGood (handler.mkcases x)
     | Quit x       -> mkGood (handler.quit x)
     | About x      -> mkGood (handler.about x)
@@ -766,7 +759,6 @@ let of_answer (q : 'a call) (v : 'a value) : xml = match q with
   | Search _     -> of_value (of_value_type search_rty_t     ) (Obj.magic v)
   | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v)
   | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v)
-  | InLoadPath _ -> of_value (of_value_type inloadpath_rty_t ) (Obj.magic v)
   | MkCases _    -> of_value (of_value_type mkcases_rty_t    ) (Obj.magic v)
   | Quit _       -> of_value (of_value_type quit_rty_t       ) (Obj.magic v)
   | About _      -> of_value (of_value_type about_rty_t      ) (Obj.magic v)
@@ -785,7 +777,6 @@ let to_answer (q : 'a call) (x : xml) : 'a value = match q with
   | Search _     -> Obj.magic (to_value (to_value_type search_rty_t     ) x)
   | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x)
   | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x)
-  | InLoadPath _ -> Obj.magic (to_value (to_value_type inloadpath_rty_t ) x)
   | MkCases _    -> Obj.magic (to_value (to_value_type mkcases_rty_t    ) x)
   | Quit _       -> Obj.magic (to_value (to_value_type quit_rty_t       ) x)
   | About _      -> Obj.magic (to_value (to_value_type about_rty_t      ) x)
@@ -806,7 +797,6 @@ let of_call (q : 'a call) : xml =
   | Search x     -> mkCall (of_value_type search_sty_t      x) 
   | GetOptions x -> mkCall (of_value_type get_options_sty_t x) 
   | SetOptions x -> mkCall (of_value_type set_options_sty_t x) 
-  | InLoadPath x -> mkCall (of_value_type inloadpath_sty_t  x) 
   | MkCases x    -> mkCall (of_value_type mkcases_sty_t     x) 
   | Quit x       -> mkCall (of_value_type quit_sty_t        x) 
   | About x      -> mkCall (of_value_type about_sty_t       x) 
@@ -828,7 +818,6 @@ let to_call : xml -> unknown call =
     | "Search"     -> Search     (mkCallArg search_sty_t      a)
     | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a)
     | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a)
-    | "InLoadPath" -> InLoadPath (mkCallArg inloadpath_sty_t  a)
     | "MkCases"    -> MkCases    (mkCallArg mkcases_sty_t     a)
     | "Quit"       -> Quit       (mkCallArg quit_sty_t        a)
     | "About"      -> About      (mkCallArg about_sty_t       a)
@@ -864,7 +853,6 @@ let pr_full_value call value = match call with
   | Search _     -> pr_value_gen (print search_rty_t     ) (Obj.magic value) 
   | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value) 
   | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value) 
-  | InLoadPath _ -> pr_value_gen (print inloadpath_rty_t ) (Obj.magic value) 
   | MkCases _    -> pr_value_gen (print mkcases_rty_t    ) (Obj.magic value) 
   | Quit _       -> pr_value_gen (print quit_rty_t       ) (Obj.magic value) 
   | About _      -> pr_value_gen (print about_rty_t      ) (Obj.magic value) 
@@ -882,7 +870,6 @@ let pr_call call = match call with
   | Search x     -> str_of_call call ^ " " ^ print search_sty_t      x
   | GetOptions x -> str_of_call call ^ " " ^ print get_options_sty_t x
   | SetOptions x -> str_of_call call ^ " " ^ print set_options_sty_t x
-  | InLoadPath x -> str_of_call call ^ " " ^ print inloadpath_sty_t  x
   | MkCases x    -> str_of_call call ^ " " ^ print mkcases_sty_t     x
   | Quit x       -> str_of_call call ^ " " ^ print quit_sty_t        x
   | About x      -> str_of_call call ^ " " ^ print about_sty_t       x
diff --git a/lib/serialize.mli b/lib/serialize.mli
index db92dc9eaa..b8bb1a33a3 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -21,7 +21,6 @@ val query       : query_sty       -> query_rty call
 val goals       : goals_sty       -> goals_rty call
 val hints       : hints_sty       -> hints_rty call
 val status      : status_sty      -> status_rty call
-val inloadpath  : inloadpath_sty  -> inloadpath_rty call
 val mkcases     : mkcases_sty     -> mkcases_rty call
 val evars       : evars_sty       -> evars_rty call
 val search      : search_sty      -> search_rty call
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 1b97a69ba1..8ea5de3654 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 9cb5e9511e..c612586557 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 1eba274ab2..cd9245895b 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 11cb726c77..27509fcc09 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 37f4266d04..cb6e601362 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)