diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 23 |
1 files changed, 23 insertions, 0 deletions
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} |