diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-12 17:39:42 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-12 17:39:42 +0100 |
| commit | a67c3fe2a5445bf2be94e654aac6ea328cbcd74e (patch) | |
| tree | f549e2726eca0966bde5c085ddc09a4921788a4d /ide/coq.mli | |
| parent | a622c4c951f559fa05d45a45b4b25ace00793281 (diff) | |
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.
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 0b246b842..542cc4462 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 |