From 404c0f9c6b189c4273a9bc1698765eaa6a664389 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 18 Mar 2011 11:03:03 +0000
Subject: 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
---
 proofs/refiner.ml  | 21 +++++++++++++++++++++
 proofs/refiner.mli |  1 +
 proofs/tacexpr.ml  |  1 +
 3 files changed, 23 insertions(+)

(limited to 'proofs')

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
-- 
cgit v1.2.3