diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 23 |
2 files changed, 26 insertions, 0 deletions
@@ -16,6 +16,9 @@ Tactics - New tactics constr_eq, is_evar and has_evar. - Remove the two-argument variant of "decide equality". +- New experimental tactical "timeout <n> <tac>". Since <n> is a time + in second for the moment, this feature should rather be avoided + in scripts meant to be machine-independent. Vernacular commands diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 090bbb0a92..793c364dea 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -100,6 +100,7 @@ is understood as & | & {\tt progress} {\tacexprpref}\\ & | & {\tt repeat} {\tacexprpref}\\ & | & {\tt try} {\tacexprpref}\\ +& | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ & | & {\tacexprinf} \\ \\ {\tacexprinf} & ::= & @@ -443,6 +444,28 @@ This is a combination of the previous variants. \ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}. +\subsubsection[Timeout]{Timeout\tacindex{timeout} +\index{Tacticals!timeout@{\tt timeout}}} + +We can force a tactic to stop if it has not finished after a certain +amount of time: +\begin{quote} +{\tt timeout} {\num} {\tacexpr} +\end{quote} +{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +normally applied, except that it is interrupted after ${\num}$ seconds +if it is still running. In this case the outcome is a failure. + +Warning: For the moment, {\tt timeout} is based on elapsed time in +seconds, which is very +machine-dependent: a script that works on a quick machine may fail +on a slow one. The converse is even possible if you combine a +{\tt timeout} with some other tacticals. This tactical is hence +proposed only for convenience during debug or other development +phases, we strongly advise you to not leave any {\tt timeout} in +final scripts. Note also that this tactical isn't available on +the native Windows port of Coq. + \subsubsection[Local definitions]{Local definitions\index{Ltac!let} \index{Ltac!let rec} \index{let!in Ltac} |