diff options
| -rw-r--r-- | parsing/g_ltac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 4 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 21 | ||||
| -rw-r--r-- | proofs/refiner.mli | 1 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 1 |
8 files changed, 35 insertions, 0 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 1d100c7cc4..e71d53bf96 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -57,6 +57,7 @@ GEXTEND Gram | "3" RIGHTA [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) + | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta (*To do: put Abstract in Refiner*) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 9da14d8fa6..b781e4e6e2 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -888,6 +888,10 @@ let rec pr_tac inherited tac = hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ pr_tac (ltactical,E) t), ltactical + | TacTimeout (n,t) -> + hov 1 (str "timeout " ++ pr_or_var int n ++ spc () ++ + pr_tac (ltactical,E) t), + ltactical | TacRepeat t -> hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t), ltactical diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index eceb02d53e..a155015b5f 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -428,6 +428,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacOrelse $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >> | Tacexpr.TacDo (n,t) -> <:expr< Tacexpr.TacDo $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >> + | Tacexpr.TacTimeout (n,t) -> + <:expr< Tacexpr.TacTimeout $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >> | Tacexpr.TacRepeat t -> <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >> | Tacexpr.TacProgress t -> 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 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 73d56053da..505ab161bf 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -842,6 +842,8 @@ and intern_tactic_seq ist = function lfun', TacThens (t, List.map (intern_tactic ist') tl) | TacDo (n,tac) -> ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac) + | TacTimeout (n,tac) -> + ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic ist tac) | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac) | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac) | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac) @@ -1810,6 +1812,7 @@ and eval_tactic ist = function (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl) | TacThens (t1,tl) -> tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) | TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac) + | TacTimeout (n,tac) -> tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) | TacTry tac -> tclTRY (interp_tactic ist tac) | TacInfo tac -> let t = (interp_tactic ist tac) in @@ -2749,6 +2752,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacThens (t,tl) -> TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl) | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac) + | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac) | TacTry tac -> TacTry (subst_tactic subst tac) | TacInfo tac -> TacInfo (subst_tactic subst tac) | TacRepeat tac -> TacRepeat (subst_tactic subst tac) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 2598cab5e2..e2e6e3a71c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -59,6 +59,7 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE let tclFAIL = Refiner.tclFAIL let tclFAIL_lazy = Refiner.tclFAIL_lazy let tclDO = Refiner.tclDO +let tclTIMEOUT = Refiner.tclTIMEOUT let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS let tclPROGRESS = Refiner.tclPROGRESS let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL |