lib/scripts/timestop.bash
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 60990 07592e217180
permissions -rw-r--r--
updated for release;
     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 [ ${KIND} -eq 1 -o ${TIME} -ge 5 ]; then
    38       if [ -z "$TIMES_REPORT" ]; then
    39         TIMES_REPORT="$RESULT"
    40       else
    41         TIMES_REPORT="$TIMES_REPORT, $RESULT"
    42       fi
    43     fi
    44   done
    45   if let "$TIME1 >= 5 && $TIME2 >= 5"
    46   then
    47     local FACTOR=$(( $TIME2 * 100 / $TIME1 ))
    48     local FACTOR1=$(( $FACTOR / 100 ))
    49     local FACTOR2=$(( $FACTOR % 100 ))
    50     if let "$FACTOR2 < 10"; then FACTOR2="0$FACTOR2"; fi
    51     TIMES_REPORT="$TIMES_REPORT, factor ${FACTOR1}.${FACTOR2}"
    52   fi
    53 }
    54 
    55 show_times  # sets TIMES_REPORT
    56 
    57 unset TIMES_RESULT get_times show_times