|
5.3.8 timer
Type:
- int
Purpose:
-
the CPU time (i.e, user and system time) used for each command is
printed if timer >0 , if this
time is bigger than a (customizable) minimal time and
if
printlevel+1 >= voice (which is by default true on the
SINGULAR top level, but not true while procedures are executed).
-
yields the CPU time used since the start-up of SINGULAR in a
(customizable) resolution.
The default setting of timer is 0, the default minimal time is
0.5 seconds, and the default timer resolution is 1 (i.e., the default unit
of time is one second). The minimal time and timer resolution
can be set using the command line options --min-time and
--ticks-per-sec and can be checked using
system("--min-time") and system("--ticks-per-sec") .
How to use timer in order to measure the time for a sequence of
commands, see example below.
Note for Windows95/98:
- The value of the
timer cannot be used (resp. trusted) when
SINGULAR is run under Windows95/98 (this is due to the shortcomings
of the Windows95/98 operating system). Use rtimer, instead.
Example:
See
Command line options;
printlevel;
rtimer;
system;
voice.
|