| author | sultana | 
| Sat, 14 Apr 2012 23:52:17 +0100 | |
| changeset 47477 | 3fabf352243e | 
| parent 31310 | b5365a9db718 | 
| child 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  | 
|
| 
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
37  | 
if [ -z "$TIMES_REPORT" ]; then  | 
| 
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
38  | 
TIMES_REPORT="$RESULT"  | 
| 
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
39  | 
else  | 
| 
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
40  | 
TIMES_REPORT="$TIMES_REPORT, $RESULT"  | 
| 
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
41  | 
fi  | 
| 
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
42  | 
done  | 
| 28467 | 43  | 
if let "$TIME1 >= 5 && $TIME2 >= 5"  | 
44  | 
then  | 
|
| 28469 | 45  | 
local FACTOR=$(( $TIME2 * 100 / $TIME1 ))  | 
46  | 
local FACTOR1=$(( $FACTOR / 100 ))  | 
|
47  | 
local FACTOR2=$(( $FACTOR % 100 ))  | 
|
| 28492 | 48  | 
if let "$FACTOR2 < 10"; then FACTOR2="0$FACTOR2"; fi  | 
| 28467 | 49  | 
    TIMES_REPORT="$TIMES_REPORT, factor ${FACTOR1}.${FACTOR2}"
 | 
50  | 
fi  | 
|
| 
18318
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
51  | 
}  | 
| 
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
52  | 
|
| 
 
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
 
wenzelm 
parents:  
diff
changeset
 | 
53  | 
show_times # sets TIMES_REPORT  | 
| 
 
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  | 
unset TIMES_RESULT get_times show_times  |