From b8890796f260449084d5be3c036f9c479c38a5ce Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 10 Jan 2020 19:38:43 +0000 Subject: [PATCH] jobs: Wait for completion even in the error case. Previously if we hit an error (last_exn being set) then we exited the loop immediately and re-raised the exception. However this means jobs which are still running would continue to run after goals exited. Move the wait code outside the loop to ensure we always wait for jobs to complete even in the error case. --- src/jobs.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/jobs.ml b/src/jobs.ml index 085d466..2e8735e 100644 --- a/src/jobs.ml +++ b/src/jobs.ml @@ -52,13 +52,7 @@ let run next_job retire_job string_of_job = let rec loop () = if !last_exn = None then ( match next_job () with - | Complete -> - if !running > 0 then ( - Cmdline.debug "%d/%d threads running, waiting for completion" - !running (Cmdline.nr_jobs ()); - Condition.wait cond lock; - loop () - ) + | Complete -> () | Not_ready -> assert (!running > 0); Cmdline.debug "%d/%d threads running, waiting for dependencies" @@ -80,6 +74,14 @@ let run next_job retire_job string_of_job = in Mutex.lock lock; loop (); + + (* Wait for all jobs to complete. *) + while !running > 0 do + Cmdline.debug "%d/%d threads running, waiting for completion" + !running (Cmdline.nr_jobs ()); + Condition.wait cond lock + done; + let exn = !last_exn in Mutex.unlock lock; -- 1.8.3.1