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.
---
 lib/interface.mli | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'lib/interface.mli')

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