Admin/isatest-stats
author wenzelm
Tue, 19 Sep 2006 23:12:21 +0200
changeset 20619 02e9b54b18fd
parent 20618 3f763be47c2f
child 20632 40abbc7c86df
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20613
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     2
#
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     3
# $Id$
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     4
# Author: Makarius
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     5
#
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     6
# DESCRIPTION: Standard statistics.
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     7
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     8
THIS=$(cd "$(dirname "$0")"; pwd -P)
8f2731bfe86f Standard statistics.
wenzelm
parents:
diff changeset
     9
20618
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    10
PLATFORMS="at-poly at-sml-dev"
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    11
SESSIONS="\
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    12
  HOL \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    13
  HOL-Algebra \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    14
  HOL-Auth \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    15
  HOL-Bali \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    16
  HOL-Complex \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    17
  HOL-Extraction \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    18
  HOL-Hoare \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    19
  HOL-HoareParallel \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    20
  HOL-Lambda \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    21
  HOL-MicroJava \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    22
  HOL-NumberTheory \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    23
  HOL-SET-Protocol \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    24
  HOL-UNITY \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    25
  HOL-ex \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    26
  ZF \
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    27
  ZF-Constructible"
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    28
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    29
for PLATFORM in $PLATFORMS
20615
wenzelm
parents: 20613
diff changeset
    30
do
20618
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    31
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 100 $SESSIONS
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    32
  cat > "stats/$PLATFORM.html" <<EOF
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    33
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    34
<html>
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    35
<head><title> Development Snapshot -- Statistics</title></head>
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    36
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    37
<body>
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    38
<h1>$PLATFORM</h1>
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    39
EOF
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    40
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    41
for SESSION in $SESSIONS
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    42
do
20619
wenzelm
parents: 20618
diff changeset
    43
  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
20615
wenzelm
parents: 20613
diff changeset
    44
done
20618
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    45
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    46
echo "</body>" >> "stats/$PLATFORM.html"
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    47
echo "</html>" >> "stats/$PLATFORM.html"
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    48
3f763be47c2f simple html output;
wenzelm
parents: 20617
diff changeset
    49
done