blob: 67d5a9b4edcec5f12246ab61d80aef65d1042407 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*s interruption *)
let interrupt = ref false
let steps = ref 0
let slave_process =
let rec f = ref (fun () ->
match !Flags.async_proofs_mode with
| Flags.APonParallel n -> let b = n > 0 in f := (fun () -> b); !f ()
| _ -> f := (fun () -> false); !f ()) in
fun () -> !f ()
let check_for_interrupt () =
if !interrupt then begin interrupt := false; raise Sys.Break end;
incr steps;
if !steps = 10000 && slave_process () then begin
Thread.yield ();
steps := 0;
end
(** This function does not work on windows, sigh... *)
let unix_timeout n f e =
let timeout_handler _ = raise e in
let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
let _ = Unix.alarm n in
let restore_timeout () =
let _ = Unix.alarm 0 in
Sys.set_signal Sys.sigalrm psh
in
try
let res = f () in
restore_timeout ();
res
with e ->
let e = Backtrace.add_backtrace e in
restore_timeout ();
raise e
let windows_timeout n f e =
let killed = ref false in
let exited = ref false in
let thread init =
while not !killed do
let cur = Unix.time () in
if float_of_int n <= cur -. init then begin
interrupt := true;
exited := true;
Thread.exit ()
end;
Thread.delay 0.5
done
in
let init = Unix.time () in
let _id = Thread.create thread init in
try
let res = f () in
let () = killed := true in
let cur = Unix.time () in
(** The thread did not interrupt, but the computation took longer than
expected. *)
let () = if float_of_int n <= cur -. init then begin
exited := true;
raise Sys.Break
end in
res
with
| Sys.Break ->
(** Just in case, it could be a regular Ctrl+C *)
if not !exited then begin killed := true; raise Sys.Break end
else raise e
| e ->
let () = killed := true in
let e = Backtrace.add_backtrace e in
raise e
type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }
let timeout_fun = match Sys.os_type with
| "Unix" | "Cygwin" -> ref { timeout = unix_timeout }
| _ -> ref { timeout = windows_timeout }
let set_timeout f = timeout_fun := f
let timeout n f e = !timeout_fun.timeout n f e
|