lib/scripts/timestop.bash
changeset 73400 e488f4bb1c79
parent 73399 48569c862eb8
child 73401 8b464825d2b5
equal deleted inserted replaced
73399:48569c862eb8 73400:e488f4bb1c79
     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