Protect some I/O routines from SIGALRM

This is necessary to prevent Coq from sending ill-formed output in some
scenarios involving `Timeout`.

Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>

1 files changed, 18 insertions, 0 deletions

diff --git a/lib/control.ml b/lib/control.ml
index ffb3584f1e..9054507e46 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -89,3 +89,21 @@ let timeout_fun_ref = ref timeout_fun
 let set_timeout f = timeout_fun_ref := f
 
 let timeout n f e = !timeout_fun_ref.timeout n f e
+
+let protect_sigalrm f x =
+  let timed_out = ref false in
+  let timeout_handler _ = timed_out := true in
+  try
+    let old_handler = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+    try
+      let res = f x in
+      Sys.set_signal Sys.sigalrm old_handler;
+      match !timed_out, old_handler with
+      | true, Sys.Signal_handle f -> f Sys.sigalrm; res
+      | _, _ -> res
+    with e ->
+      let e = Backtrace.add_backtrace e in
+      Sys.set_signal Sys.sigalrm old_handler;
+      Exninfo.iraise e
+  with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *)
+    f x