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, 30 insertions, 38 deletions

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