From 24a0df63c1844c6f2c69f9644a3059d668fd1e6f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 7 Jun 2014 00:28:29 +0200 Subject: Adding a new Control file centralizing the control options of Coq. --- checker/check.mllib | 1 + checker/reduction.ml | 2 +- dev/printers.mllib | 1 + kernel/reduction.ml | 2 +- lib/clib.mllib | 1 + lib/control.ml | 40 ++++++++++++++++++++++++++++++++++++ lib/control.mli | 26 ++++++++++++++++++++++++ lib/util.ml | 6 ------ lib/util.mli | 6 ------ plugins/cc/ccalgo.ml | 6 +++--- plugins/firstorder/rules.ml | 2 +- plugins/rtauto/proof_search.ml | 2 +- proofs/proofview_gen.ml | 21 +++---------------- proofs/refiner.ml | 6 +++--- tactics/tacinterp.ml | 2 +- toplevel/ide_slave.ml | 4 ++-- toplevel/vernacentries.ml | 46 ++++++++++-------------------------------- 17 files changed, 96 insertions(+), 78 deletions(-) create mode 100644 lib/control.ml create mode 100644 lib/control.mli 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 *) +(* + 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 *) +(* 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 = -- cgit v1.2.3