From 468050a3831cedf63d7dbdb289d5824097bbe1e0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jan 2019 10:54:46 +0100
Subject: [vio] free resources (file descriptors) as soon as a worker ends

---
 stm/vio_checking.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'stm')

diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 64f19e1fd9..41e11ba255 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
@@ -137,6 +138,7 @@ 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;
   exit !rc
-- 
cgit v1.2.3


From 44b5f77f36011e797f0d7d36098296dc7d6c1c51 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 11 Jan 2019 11:46:47 +0100
Subject: [STM] set the mtime of files generated via vio2vo (fix #9334)

---
 stm/vio_checking.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'stm')

diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 41e11ba255..69c1d9bd23 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -125,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;
@@ -141,6 +142,12 @@ let schedule_vio_compilation j fs =
     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
 
   
-- 
cgit v1.2.3