Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

[session] do not prepare tasks on disk too early

parent 109307fb
...@@ -235,10 +235,9 @@ let schedule_check t callback = ...@@ -235,10 +235,9 @@ let schedule_check t callback =
(* idle handler *) (* idle handler *)
let idle_handler t = let idle_handler t =
try try
begin if Queue.length t.proof_attempts_queue < 2 * t.maximum_running_proofs then begin
match Queue.pop t.actions_queue with match Queue.pop t.actions_queue with
| Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver, | Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
callback,goal) -> callback,goal) ->
...@@ -257,7 +256,8 @@ let idle_handler t = ...@@ -257,7 +256,8 @@ let idle_handler t =
callback (InternalFailure e) callback (InternalFailure e)
end end
| Action_delayed callback -> callback () | Action_delayed callback -> callback ()
end; end else
ignore (Unix.select [] [] [] 0.1);
true true
with Queue.Empty -> with Queue.Empty ->
t.idle_handler_activated <- false; t.idle_handler_activated <- false;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment