aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.mllib1
-rw-r--r--checker/reduction.ml2
-rw-r--r--dev/printers.mllib1
-rw-r--r--kernel/reduction.ml2
-rw-r--r--lib/clib.mllib1
-rw-r--r--lib/control.ml40
-rw-r--r--lib/control.mli26
-rw-r--r--lib/util.ml6
-rw-r--r--lib/util.mli6
-rw-r--r--plugins/cc/ccalgo.ml6
-rw-r--r--plugins/firstorder/rules.ml2
-rw-r--r--plugins/rtauto/proof_search.ml2
-rw-r--r--proofs/proofview_gen.ml21
-rw-r--r--proofs/refiner.ml6
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--toplevel/ide_slave.ml4
-rw-r--r--toplevel/vernacentries.ml46
17 files changed, 96 insertions, 78 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index 7488a2c57..9f0bc200c 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -12,6 +12,7 @@ Option
Store
Exninfo
Backtrace
+Control
Flags
Pp_control
Pp
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 384b9ad7f..49f0a26e7 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -226,7 +226,7 @@ let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
- Util.check_for_interrupt ();
+ Control.check_for_interrupt ();
(* First head reduce both terms *)
let rec whd_both (t1,stk1) (t2,stk2) =
let st1' = whd_stack infos t1 stk1 in
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 2eae9d598..d9f4aacce 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -12,6 +12,7 @@ Option
Store
Exninfo
Backtrace
+Control
IStream
Pp_control
Loc
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b62ca2045..c96371f26 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -289,7 +289,7 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
- Util.check_for_interrupt ();
+ Control.check_for_interrupt ();
incr steps;
if !steps = 10000 && slave_process () then begin
Thread.yield ();
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 1dc540b9a..cd8964f02 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -12,6 +12,7 @@ Option
Store
Exninfo
Backtrace
+Control
IArray
IStream
Pp_control
diff --git a/lib/control.ml b/lib/control.ml
new file mode 100644
index 000000000..9573614fd
--- /dev/null
+++ b/lib/control.ml
@@ -0,0 +1,40 @@
+(************************************************************************)
+(* 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 check_for_interrupt () =
+ if !interrupt then begin interrupt := false; raise Sys.Break 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
+
+type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }
+
+let timeout_fun = ref { timeout = unix_timeout }
+
+let set_timeout f = timeout_fun := f
+
+let timeout n f e = !timeout_fun.timeout n f e
diff --git a/lib/control.mli b/lib/control.mli
new file mode 100644
index 000000000..36c834915
--- /dev/null
+++ b/lib/control.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(** Global control of Coq. *)
+
+val interrupt : bool ref
+(** Coq interruption: set the following boolean reference to interrupt Coq
+ (it eventually raises [Break], simulating a Ctrl-C) *)
+
+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 -> (unit -> 'a) -> exn -> 'a
+(** [timeout n f e] tries to compute [f], and if it fails to do so before [n]
+ seconds, it raises [e] instead. *)
+
+type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }
+
+val set_timeout : timeout -> unit
+(** Set a particular timeout function. *)
diff --git a/lib/util.ml b/lib/util.ml
index 9ade75147..16b5f4615 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -124,9 +124,3 @@ let delayed_force f = f ()
type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
-
-(*s interruption *)
-
-let interrupt = ref false
-let check_for_interrupt () =
- if !interrupt then begin interrupt := false; raise Sys.Break end
diff --git a/lib/util.mli b/lib/util.mli
index d3e3432a3..fd766a30f 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -103,9 +103,3 @@ type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
(** Used for browsable-until structures. *)
-(** {6 ... } *)
-(** Coq interruption: set the following boolean reference to interrupt Coq
- (it eventually raises [Break], simulating a Ctrl-C) *)
-
-val interrupt : bool ref
-val check_for_interrupt : unit -> unit
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index c726fd5de..50b647e44 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -574,7 +574,7 @@ let is_redundant state id args =
with Not_found -> false
let add_inst state (inst,int_subst) =
- check_for_interrupt ();
+ Control.check_for_interrupt ();
if state.rew_depth > 0 then
if is_redundant state inst.qe_hyp_id int_subst then
debug (str "discarding redundant (dis)equality")
@@ -955,7 +955,7 @@ let find_instances state =
debug (str "Running E-matching algorithm ... ");
try
while true do
- check_for_interrupt ();
+ Control.check_for_interrupt ();
do_match state res pb_stack
done;
anomaly (Pp.str "get out of here !")
@@ -966,7 +966,7 @@ let rec execute first_run state =
debug (str "Executing ... ");
try
while
- check_for_interrupt ();
+ Control.check_for_interrupt ();
one_step state do ()
done;
match check_disequalities state with
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 996deb8c5..986f2bebc 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -27,7 +27,7 @@ type lseqtac= global_reference -> seqtac
type 'a with_backtracking = tactic -> 'a
let wrap n b continue seq gls=
- check_for_interrupt ();
+ Control.check_for_interrupt ();
let nc=pf_hyps gls in
let env=pf_env gls in
let rec aux i nc ctx=
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 1ed9b8269..2b49e0cf6 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -457,7 +457,7 @@ let success= function
let branching = function
Incomplete (seq,stack) ->
- check_for_interrupt ();
+ Control.check_for_interrupt ();
let successors = search_all seq in
let _ =
match successors with
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index a686c528c..cb195c5e8 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -75,24 +75,9 @@ module IOBase =
(** val timeout : int -> 'a1 coq_T -> 'a1 coq_T **)
let timeout = fun n t -> (); fun () ->
- let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
- let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
- Pervasives.ignore (Unix.alarm n);
- let restore_timeout () =
- Pervasives.ignore (Unix.alarm 0);
- Sys.set_signal Sys.sigalrm psh
- in
- try
- let res = t () in
- restore_timeout ();
- res
- with
- | e ->
- let e = Errors.push e in
- restore_timeout ();
- Pervasives.raise e
-
- end
+ Control.timeout n t (Proof_errors.Exception Proof_errors.Timeout)
+
+end
type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 157faae3d..f0e8bf3ec 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -44,7 +44,7 @@ let unpackage glsig = (ref (glsig.sigma)), glsig.it
let repackage r v = {it = v; sigma = !r; }
let apply_sig_tac r tac g =
- check_for_interrupt (); (* Breakpoint *)
+ Control.check_for_interrupt (); (* Breakpoint *)
let glsigma = tac (repackage r g) in
r := glsigma.sigma;
glsigma.it
@@ -219,10 +219,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
let catch_failerror e =
- if catchable_exception e then check_for_interrupt ()
+ if catchable_exception e then Control.check_for_interrupt ()
else match e with
| FailError (0,_) ->
- check_for_interrupt ()
+ Control.check_for_interrupt ()
| FailError (lvl,s) ->
raise (Exninfo.copy e (FailError (lvl - 1, s)))
| e -> raise e
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e9fbece4d..b7018fe45 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -989,7 +989,7 @@ let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument GTac.t =
(** Delayed evaluation *)
GTac.return (of_tacvalue (VFun (extract_trace ist, ist.lfun, [], t)))
in
- check_for_interrupt ();
+ Control.check_for_interrupt ();
match curr_debug ist with
| DebugOn lev ->
let eval v =
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 8ea5de365..8f2fa69a0 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -24,7 +24,7 @@ open Printer
let catch_break = ref false
let init_signal_handler () =
- let f _ = if !catch_break then raise Sys.Break else Util.interrupt := true in
+ let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in
Sys.set_signal Sys.sigint (Sys.Signal_handle f)
@@ -339,7 +339,7 @@ let quit = ref false
let eval_call xml_oc log c =
let interruptible f x =
catch_break := true;
- Util.check_for_interrupt ();
+ Control.check_for_interrupt ();
let r = f x in
catch_break := false;
let out = read_stdout () in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5864c54b6..007ab5238 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1879,32 +1879,14 @@ let _ =
let current_timeout = ref None
-(** Installing and de-installing a timer.
- Note: according to ocaml documentation, Unix.alarm isn't available
- for native win32. *)
-
-let timeout_handler _ = raise Timeout
-
-let set_timeout n =
- let psh =
- Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
- ignore (Unix.alarm n);
- Some psh
-
-let default_set_timeout () =
+let vernac_timeout f =
match !current_timeout, !default_timeout with
- | Some n, _ -> set_timeout n
- | None, Some n -> set_timeout n
- | None, None -> None
-
-let restore_timeout = function
- | None -> ()
- | Some psh ->
- (* stop alarm *)
- ignore(Unix.alarm 0);
- (* restore handler *)
- Sys.set_signal Sys.sigalrm psh;
- current_timeout := None
+ | Some n, _ | None, Some n ->
+ let f () = f (); current_timeout := None in
+ Control.timeout n f Timeout
+ | None, None -> f ()
+
+let restore_timeout () = current_timeout := None
let locate_if_not_already loc exn =
match Loc.get_loc exn with
@@ -1969,24 +1951,18 @@ let interp ?(verbosely=true) ?proof (loc,c) =
check_vernac_supports_polymorphism c polymorphism;
let poly = enforce_polymorphism polymorphism in
Obligations.set_program_mode isprogcmd;
- let psh = default_set_timeout () in
try
+ vernac_timeout begin fun () ->
if verbosely then Flags.verbosely (interp ?proof locality poly) c
else Flags.silently (interp ?proof locality poly) c;
- restore_timeout psh;
if orig_program_mode || not !Flags.program_mode || isprogcmd then
Flags.program_mode := orig_program_mode
+ end
with
- | reraise when Errors.noncritical reraise ->
- let e = Errors.push reraise in
- let e = locate_if_not_already loc e in
- restore_timeout psh;
- Flags.program_mode := orig_program_mode;
- raise e
- | Timeout as reraise ->
+ | reraise when (match reraise with Timeout _ -> true | e -> Errors.noncritical e) ->
let e = Errors.push reraise in
let e = locate_if_not_already loc e in
- restore_timeout psh;
+ let () = restore_timeout () in
Flags.program_mode := orig_program_mode;
raise e
and aux_list ?locality ?polymorphism isprogcmd l =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 13:12:58 +0000