Add support for high resolution timeout functions.

6 files changed, 15 insertions, 11 deletions

diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 7784b38c80..5208469082 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -74,7 +74,7 @@ module NonLogical : sig
 
   (** [try ... with ...] but restricted to {!Exception}. *)
   val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val timeout : int -> 'a t -> 'a option t
+  val timeout : float -> 'a t -> 'a option t
 
   (** Construct a monadified side-effect. Exceptions raised by the argument are
       wrapped with {!Exception}. *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 22863f451d..a4d96a7e8f 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -926,7 +926,7 @@ let _ = CErrors.register_handler begin function
   | _ -> None
 end
 
-let tclTIMEOUT n t =
+let tclTIMEOUTF n t =
   let open Proof in
   (* spiwack: as one of the monad is a continuation passing monad, it
      doesn't force the computation to be threaded inside the underlying
@@ -951,6 +951,8 @@ let tclTIMEOUT n t =
         return res
     | Util.Inr (e, info) -> tclZERO ~info e
 
+let tclTIMEOUT n t = tclTIMEOUTF (float_of_int n) t
+
 let tclTIME s t =
   let pr_time t1 t2 n msg =
     let msg =
diff --git a/engine/proofview.mli b/engine/proofview.mli
index fe0d7ae51e..bf6021b1b6 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -418,7 +418,8 @@ val tclCHECKINTERRUPT : unit tactic
 
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout it fails with [tclZERO Tac_Timeout]. *)
-val tclTIMEOUT : int -> 'a tactic -> 'a tactic
+val tclTIMEOUTF : float -> 'a tactic -> 'a tactic
+val tclTIMEOUT  : int   -> 'a tactic -> 'a tactic
 
 (** [tclTIME s t] displays time for each atomic call to t, using s as an
     identifying annotation if present *)
diff --git a/lib/control.ml b/lib/control.ml
index 7da95ff3dd..ea94bda064 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -30,11 +30,12 @@ let check_for_interrupt () =
 
 (** This function does not work on windows, sigh... *)
 let unix_timeout n f x =
+  let open Unix in
   let timeout_handler _ = raise Timeout in
   let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-  let _ = Unix.alarm n in
+  let _ = setitimer ITIMER_REAL {it_interval = 0.; it_value = n} in
   let restore_timeout () =
-    let _ = Unix.alarm 0 in
+    let _ = setitimer ITIMER_REAL { it_interval = 0.; it_value = 0. } in
     Sys.set_signal Sys.sigalrm psh
   in
   try
@@ -52,7 +53,7 @@ let windows_timeout n f x =
   let thread init =
     while not !killed do
       let cur = Unix.gettimeofday () in
-      if float_of_int n <= cur -. init then begin
+      if n <= cur -. init then begin
         interrupt := true;
         exited := true;
         Thread.exit ()
@@ -68,7 +69,7 @@ let windows_timeout n f x =
     let cur = Unix.gettimeofday () in
     (* The thread did not interrupt, but the computation took longer than
        expected. *)
-    let () = if float_of_int n <= cur -. init then begin
+    let () = if n <= cur -. init then begin
       exited := true;
       raise Sys.Break
     end in
@@ -83,7 +84,7 @@ let windows_timeout n f x =
     let () = killed := true in
     Exninfo.iraise e
 
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
+type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option }
 
 let timeout_fun = match Sys.os_type with
 | "Unix" | "Cygwin" -> { timeout = unix_timeout }
diff --git a/lib/control.mli b/lib/control.mli
index 9465d8f0d5..f992d8e8d0 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -24,13 +24,13 @@ val check_for_interrupt : unit -> unit
 (** Use this function as a potential yield function. If {!interrupt} has been
     set, il will raise [Sys.Break]. *)
 
-val timeout : int -> ('a -> 'b) -> 'a -> 'b option
+val timeout : float -> ('a -> 'b) -> 'a -> 'b option
 (** [timeout n f x] tries to compute [Some (f x)], and if it fails to do so
     before [n] seconds, returns [None] instead. *)
 
 (** Set a particular timeout function; warning, this is an internal
    API and it is scheduled to go away. *)
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
+type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option }
 val set_timeout : timeout -> unit
 
 (** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index e5971e1aaa..3a8a80d25a 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -82,7 +82,7 @@ let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
   match !default_timeout, timeout with
   | _, Some n
   | Some n, None ->
-    (match Control.timeout n f x with
+    (match Control.timeout (float_of_int n) f x with
     | None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout)
     | Some x -> x)
   | None, None ->