Merge PR #9326: [ci] compile with -quick & validate after vio2vo

Reviewed-by: ejgallego
Ack-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot

1 files changed, 9 insertions, 0 deletions

diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 64f19e1fd9..69c1d9bd23 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -95,6 +95,7 @@ let schedule_vio_checking j fs =
     done;
     let pid, ret = Unix.wait () in
     if ret <> Unix.WEXITED 0 then rc := 1;
+    Worker.kill (Pool.find pid !pool);
     pool := Pool.remove pid !pool;
   done;
   exit !rc
@@ -124,6 +125,7 @@ let schedule_vio_compilation j fs =
     | s :: rest -> s :: filter_argv b rest in
   let prog = Sys.argv.(0) in  
   let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
+  let all_jobs = !jobs in
   let make_job () =
     let f, t = List.hd !jobs in
     jobs := List.tl !jobs;
@@ -137,8 +139,15 @@ let schedule_vio_compilation j fs =
     done;
     let pid, ret = Unix.wait () in
     if ret <> Unix.WEXITED 0 then rc := 1;
+    Worker.kill (Pool.find pid !pool);
     pool := Pool.remove pid !pool;
   done;
+  if !rc = 0 then begin
+    (* set the access and last modification time of all files to the same t
+     * not to confuse make into thinking that some of them are outdated *)
+    let t = Unix.gettimeofday () in
+    List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs;
+  end;
   exit !rc