Admin/isatest/isatest-stats
author wenzelm
Fri May 30 01:46:52 2008 +0200 (2008-05-30)
changeset 27023 6b2386074e5c
parent 26172 fa302c5bc2f2
child 27028 12c329e4d1cc
permissions -rwxr-xr-x
more AFP sessions;
kleing@22410
     1
#!/usr/bin/env bash
kleing@22410
     2
#
kleing@22410
     3
# $Id$
kleing@22410
     4
# Author: Makarius
kleing@22410
     5
#
kleing@22410
     6
# DESCRIPTION: Standard statistics.
kleing@22410
     7
kleing@22410
     8
THIS=$(cd "$(dirname "$0")"; pwd -P)
kleing@22410
     9
wenzelm@25547
    10
PLATFORMS="at-poly at-sml-dev at64-poly at64-poly-5.1-para at-mac-poly-5.1-para afp"
wenzelm@24831
    11
wenzelm@24831
    12
ISABELLE_SESSIONS="\
kleing@22410
    13
  HOL \
kleing@22410
    14
  HOL-Algebra \
kleing@22410
    15
  HOL-Auth \
kleing@22410
    16
  HOL-Bali \
kleing@22410
    17
  HOL-Complex \
kleing@22410
    18
  HOL-Complex-ex \
kleing@22410
    19
  HOL-Extraction \
kleing@22410
    20
  HOL-Hoare \
kleing@22410
    21
  HOL-HoareParallel \
kleing@22410
    22
  HOL-Lambda \
wenzelm@26172
    23
  HOL-Library \
wenzelm@24489
    24
  HOL-MetisExamples \
kleing@22410
    25
  HOL-MicroJava \
wenzelm@23443
    26
  HOL-Nominal-Examples \
kleing@22410
    27
  HOL-NumberTheory \
kleing@22410
    28
  HOL-SET-Protocol \
kleing@22410
    29
  HOL-UNITY \
kleing@22410
    30
  HOL-ex \
kleing@22410
    31
  ZF \
kleing@22410
    32
  ZF-Constructible\
kleing@22410
    33
  ZF-UNITY"
kleing@22410
    34
wenzelm@24831
    35
AFP_SESSIONS="\
wenzelm@24831
    36
  CoreC++\
wenzelm@24831
    37
  HOL-DiskPaxos\
wenzelm@24831
    38
  HOL-Fermat3_4\
wenzelm@24831
    39
  HOL-Flyspeck-Tame\
wenzelm@24831
    40
  HOL-Group-Ring-Module\
wenzelm@24831
    41
  HOL-Jinja\
wenzelm@27023
    42
  HOL-JinjaThreads\
wenzelm@24831
    43
  HOL-JiveDataStoreModel\
wenzelm@27023
    44
  HOL-LinearQuantifierElim\
wenzelm@24831
    45
  HOL-POPLmark-deBruijn\
wenzelm@24831
    46
  HOL-RSAPSS\
wenzelm@24831
    47
  HOL-SumSquares\
wenzelm@27023
    48
  HOL-Valuation\
wenzelm@27023
    49
  Simpl\
wenzelm@27023
    50
  Simpl-BDD"
wenzelm@24831
    51
kleing@22410
    52
for PLATFORM in $PLATFORMS
kleing@22410
    53
do
wenzelm@24831
    54
  if [ "$PLATFORM" = afp ]; then
wenzelm@24831
    55
    SESSIONS="$AFP_SESSIONS"
wenzelm@24831
    56
  else
wenzelm@24831
    57
    SESSIONS="$ISABELLE_SESSIONS"
wenzelm@24831
    58
  fi
wenzelm@24831
    59
kleing@22410
    60
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
kleing@22410
    61
  cat > "stats/$PLATFORM.html" <<EOF
kleing@22410
    62
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
kleing@22410
    63
<html>
kleing@22410
    64
<head><title>Development Snapshot -- Performance Statistics</title></head>
kleing@22410
    65
kleing@22410
    66
<body>
kleing@22410
    67
<h1>$PLATFORM</h1>
kleing@22410
    68
EOF
kleing@22410
    69
kleing@22410
    70
for SESSION in $SESSIONS
kleing@22410
    71
do
kleing@22410
    72
  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
kleing@22410
    73
done
kleing@22410
    74
kleing@22410
    75
echo "</body>" >> "stats/$PLATFORM.html"
kleing@22410
    76
echo "</html>" >> "stats/$PLATFORM.html"
kleing@22410
    77
kleing@22410
    78
done