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