diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-18 11:03:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-18 11:03:03 +0000 |
| commit | 404c0f9c6b189c4273a9bc1698765eaa6a664389 (patch) | |
| tree | b4465ccce38000ffb63487e86e709bd15fe54d90 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 1 |
2 files changed, 5 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 73d56053d..505ab161b 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 2598cab5e..e2e6e3a71 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 |