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