author | wenzelm |
Thu, 20 Apr 2017 17:50:31 +0200 | |
changeset 65527 | 0d8a7013bf36 |
parent 60990 | 07592e217180 |
permissions | -rw-r--r-- |
31310 | 1 |
# -*- shell-script -*- :mode=shellscript: |
29145 | 2 |
# |
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
3 |
# Author: Makarius |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
4 |
# |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
5 |
# timestop - report timing based on environment (cf. timestart.bash) |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
6 |
# |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
7 |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
8 |
TIMES_REPORT="" |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
9 |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
10 |
function show_times () |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
11 |
{ |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
12 |
local TIMES_START="$TIMES_RESULT" |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
13 |
get_times |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
14 |
local TIMES_STOP="$TIMES_RESULT" |
28467 | 15 |
local TIME1 |
16 |
local TIME2 |
|
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
17 |
local KIND |
18322 | 18 |
for KIND in 1 2 |
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
19 |
do |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
20 |
local START=$(echo "$TIMES_START" | cut -d " " -f $KIND) |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
21 |
local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND) |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
22 |
|
28467 | 23 |
local TIME=$(( $STOP - $START )) |
24 |
eval "TIME${KIND}=$TIME" |
|
25 |
||
26 |
local SECS=$(( $TIME % 60 )) |
|
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
27 |
[ $SECS -lt 10 ] && SECS="0$SECS" |
28467 | 28 |
local MINUTES=$(( ($TIME / 60) % 60 )) |
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
29 |
[ $MINUTES -lt 10 ] && MINUTES="0$MINUTES" |
28467 | 30 |
local HOURS=$(( $TIME / 3600 )) |
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
31 |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
32 |
local KIND_NAME |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
33 |
[ "$KIND" = 1 ] && KIND_NAME="elapsed time" |
18322 | 34 |
[ "$KIND" = 2 ] && KIND_NAME="cpu time" |
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
35 |
local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
36 |
|
60990
07592e217180
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
wenzelm
parents:
31310
diff
changeset
|
37 |
if [ ${KIND} -eq 1 -o ${TIME} -ge 5 ]; then |
07592e217180
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
wenzelm
parents:
31310
diff
changeset
|
38 |
if [ -z "$TIMES_REPORT" ]; then |
07592e217180
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
wenzelm
parents:
31310
diff
changeset
|
39 |
TIMES_REPORT="$RESULT" |
07592e217180
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
wenzelm
parents:
31310
diff
changeset
|
40 |
else |
07592e217180
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
wenzelm
parents:
31310
diff
changeset
|
41 |
TIMES_REPORT="$TIMES_REPORT, $RESULT" |
07592e217180
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
wenzelm
parents:
31310
diff
changeset
|
42 |
fi |
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
43 |
fi |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
44 |
done |
28467 | 45 |
if let "$TIME1 >= 5 && $TIME2 >= 5" |
46 |
then |
|
28469 | 47 |
local FACTOR=$(( $TIME2 * 100 / $TIME1 )) |
48 |
local FACTOR1=$(( $FACTOR / 100 )) |
|
49 |
local FACTOR2=$(( $FACTOR % 100 )) |
|
28492 | 50 |
if let "$FACTOR2 < 10"; then FACTOR2="0$FACTOR2"; fi |
28467 | 51 |
TIMES_REPORT="$TIMES_REPORT, factor ${FACTOR1}.${FACTOR2}" |
52 |
fi |
|
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
53 |
} |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
54 |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
55 |
show_times # sets TIMES_REPORT |
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
56 |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
57 |
unset TIMES_RESULT get_times show_times |