1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC time
\TYPE {time : ('a -> 'b) -> 'a -> 'b}
\SYNOPSIS
Report CPU time taken by a function.
\DESCRIBE
A call {time f x} will evaluate {f x} as usual, but will also (provided the
{report_timing} flag is {true} as it is by default) print the CPU time taken by
that function evaluation.
\FAILURE
Never fails in itself, though it propagates any exception generated by the call
{f x} itself.
\EXAMPLE
{
# time NUM_REDUCE_CONV `123 EXP 14`;;
CPU time (user): 0.09
val it : thm = |- 123 EXP 14 = 181414317867238075368413196009
}
\USES
Monitoring CPU time taken, e.g. to test different algorithms or implementation
optimizations.
\SEEALSO
report_timing.
\ENDDOC
|
