From def8695f2bc782438e6371084adc25e7d6f7fe13 Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Fri, 7 Mar 2014 15:48:11 +0100
Subject: [PATCH] [session] do not prepare tasks on disk too early

---
 src/session/session_scheduler.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml
index b47f9ea80..b6e34fc6d 100644
--- a/src/session/session_scheduler.ml
+++ b/src/session/session_scheduler.ml
@@ -235,10 +235,9 @@ let schedule_check t callback =
 
 (* idle handler *)
 
-
 let idle_handler t =
   try
-    begin
+    if Queue.length t.proof_attempts_queue < 2 * t.maximum_running_proofs then begin
       match Queue.pop t.actions_queue with
         | Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
                                callback,goal) ->
@@ -257,7 +256,8 @@ let idle_handler t =
                 callback (InternalFailure e)
             end
         | Action_delayed callback -> callback ()
-    end;
+    end else
+      ignore (Unix.select [] [] [] 0.1);
     true
   with Queue.Empty ->
     t.idle_handler_activated <- false;
-- 
GitLab