From a67c3fe2a5445bf2be94e654aac6ea328cbcd74e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 12 Mar 2014 17:39:42 +0100
Subject: 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.
---
 ide/coq.ml    |  1 -
 ide/coq.mli   |  1 -
 ide/coqOps.ml | 29 ++---------------------------
 3 files changed, 2 insertions(+), 29 deletions(-)

(limited to 'ide')

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
-- 
cgit v1.2.3