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