diff options
| author | letouzey | 2011-03-18 11:03:03 +0000 |
|---|---|---|
| committer | letouzey | 2011-03-18 11:03:03 +0000 |
| commit | 404c0f9c6b189c4273a9bc1698765eaa6a664389 (patch) | |
| tree | b4465ccce38000ffb63487e86e709bd15fe54d90 /proofs | |
| parent | a2f26ddde0c5ee088a4a65ab9708085c16a8ba48 (diff) | |
A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds
Note: even if this new tactical can be quite handy during the development phase,
(for instance to bound the time allocated to some search tactics), please be aware
of its main drawback: with it, scripts are no longer machine-independant, something
that works on a quick machine may fail on a slow one. The converse is even possible
if you combine this "timeout" with other tactic combinators. We strongly advise to
not leave any "timeout" in the final version of a development.
In addition, this feature won't probably work on native win32, since Unix.alarm
isn't implemented.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13917 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 21 | ||||
| -rw-r--r-- | proofs/refiner.mli | 1 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 1 |
3 files changed, 23 insertions, 0 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index eeccbd0e52..5cd855476c 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -332,6 +332,27 @@ let tclDO n t = in dorec n +(* Fails if a tactic hasn't finished after a certain amount of time *) + +exception TacTimeout + +let tclTIMEOUT n t g = + let timeout_handler _ = raise TacTimeout in + let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + ignore (Unix.alarm n); + let restore_timeout () = + ignore (Unix.alarm 0); + Sys.set_signal Sys.sigalrm psh + in + try + let res = t g in + restore_timeout (); + res + with + | TacTimeout | Loc.Exc_located(_,TacTimeout) -> + restore_timeout (); + errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!") + | e -> restore_timeout (); raise e (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index f8990a9a59..75fd6d3d65 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -133,6 +133,7 @@ val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> Pp.std_ppcmds -> tactic val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic +val tclTIMEOUT : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b37460e483..1928f5853d 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -229,6 +229,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr = | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacTimeout of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option |