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.

1 files changed, 16 insertions, 6 deletions

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;