Admin/isatest/isatest-stats
author wenzelm
Sun Jun 14 02:38:09 2009 +0200 (2009-06-14)
changeset 31620 b0f6168d2b25
parent 30700 dc38bb27df50
child 31802 a36b5e02c1ab
permissions -rwxr-xr-x
more isatest platforms;
kleing@22410
     1
#!/usr/bin/env bash
kleing@22410
     2
#
kleing@22410
     3
# Author: Makarius
kleing@22410
     4
#
kleing@22410
     5
# DESCRIPTION: Standard statistics.
kleing@22410
     6
kleing@22410
     7
THIS=$(cd "$(dirname "$0")"; pwd -P)
kleing@22410
     8
wenzelm@31620
     9
PLATFORMS="at-poly at64-poly mac-poly-M4 mac-poly-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
wenzelm@24831
    10
wenzelm@24831
    11
ISABELLE_SESSIONS="\
wenzelm@27448
    12
  HOL-Plain \
wenzelm@28530
    13
  HOL-Main \
kleing@22410
    14
  HOL \
kleing@22410
    15
  HOL-Algebra \
kleing@22410
    16
  HOL-Auth \
kleing@22410
    17
  HOL-Bali \
wenzelm@30111
    18
  HOL-Decision_Procs \
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@27478
    26
  HOL-NSA \
wenzelm@23443
    27
  HOL-Nominal-Examples \
kleing@22410
    28
  HOL-NumberTheory \
kleing@22410
    29
  HOL-SET-Protocol \
kleing@22410
    30
  HOL-UNITY \
wenzelm@27478
    31
  HOL-Word \
kleing@22410
    32
  HOL-ex \
wenzelm@30616
    33
  HOLCF \
wenzelm@30616
    34
  IOA \
kleing@22410
    35
  ZF \
wenzelm@29283
    36
  ZF-Constructible \
kleing@22410
    37
  ZF-UNITY"
kleing@22410
    38
wenzelm@24831
    39
AFP_SESSIONS="\
wenzelm@29283
    40
  CoreC++ \
wenzelm@29283
    41
  HOL-BytecodeLogicJmlTypes \
wenzelm@29283
    42
  HOL-DiskPaxos \
wenzelm@29283
    43
  HOL-Fermat3_4 \
wenzelm@29283
    44
  HOL-Flyspeck-Tame \
wenzelm@29283
    45
  HOL-Group-Ring-Module \
wenzelm@29283
    46
  HOL-Jinja \
wenzelm@29283
    47
  HOL-JinjaThreads \
wenzelm@29283
    48
  HOL-JiveDataStoreModel \
wenzelm@29283
    49
  HOL-POPLmark-deBruijn \
wenzelm@29283
    50
  HOL-Program-Conflict-Analysis \
wenzelm@29283
    51
  HOL-RSAPSS \
wenzelm@29283
    52
  HOL-Recursion-Theory-I \
wenzelm@29283
    53
  HOL-SATSolverVerification \
wenzelm@29283
    54
  HOL-SIFPL \
wenzelm@29283
    55
  HOL-SenSocialChoice \
wenzelm@29283
    56
  HOL-Slicing \
wenzelm@29283
    57
  HOL-SumSquares \
wenzelm@29283
    58
  HOL-Topology \
wenzelm@29283
    59
  HOL-Valuation \
wenzelm@29283
    60
  LinearQuantifierElim \
wenzelm@29283
    61
  Simpl \
wenzelm@29283
    62
  Simpl-BDD"
wenzelm@24831
    63
kleing@22410
    64
for PLATFORM in $PLATFORMS
kleing@22410
    65
do
wenzelm@24831
    66
  if [ "$PLATFORM" = afp ]; then
wenzelm@24831
    67
    SESSIONS="$AFP_SESSIONS"
wenzelm@24831
    68
  else
wenzelm@24831
    69
    SESSIONS="$ISABELLE_SESSIONS"
wenzelm@24831
    70
  fi
wenzelm@24831
    71
kleing@22410
    72
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
kleing@22410
    73
  cat > "stats/$PLATFORM.html" <<EOF
kleing@22410
    74
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
kleing@22410
    75
<html>
kleing@22410
    76
<head><title>Development Snapshot -- Performance Statistics</title></head>
kleing@22410
    77
kleing@22410
    78
<body>
kleing@22410
    79
<h1>$PLATFORM</h1>
kleing@22410
    80
EOF
kleing@22410
    81
kleing@22410
    82
for SESSION in $SESSIONS
kleing@22410
    83
do
kleing@22410
    84
  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
kleing@22410
    85
done
kleing@22410
    86
kleing@22410
    87
echo "</body>" >> "stats/$PLATFORM.html"
kleing@22410
    88
echo "</html>" >> "stats/$PLATFORM.html"
kleing@22410
    89
kleing@22410
    90
done