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/aux_file.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'lib/aux_file.mli') diff --git a/lib/aux_file.mli b/lib/aux_file.mli index b24515c99..f31b23408 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 -- cgit v1.2.3