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

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