Admin/isatest/isatest-stats
author wenzelm
Mon Sep 19 22:45:57 2011 +0200 (2011-09-19)
changeset 44993 9a2d100dd3eb
parent 44152 a07748619f53
child 45142 97e81a8aa277
permissions -rwxr-xr-x
more isatest stats;
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
wenzelm@44152
     7
THIS="$(cd "$(dirname "$0")"; pwd)"
kleing@22410
     8
wenzelm@44993
     9
PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para 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 \
wenzelm@34237
    15
  HOL-Proofs \
wenzelm@37976
    16
  HOL-Library \
kleing@22410
    17
  HOL-Algebra \
kleing@22410
    18
  HOL-Auth \
kleing@22410
    19
  HOL-Bali \
wenzelm@30111
    20
  HOL-Decision_Procs \
kleing@22410
    21
  HOL-Hoare \
wenzelm@33072
    22
  HOL-Hoare_Parallel \
wenzelm@37976
    23
  HOL-Imperative_HOL \
wenzelm@33027
    24
  HOL-Metis_Examples \
kleing@22410
    25
  HOL-MicroJava \
wenzelm@34237
    26
  HOL-Multivariate_Analysis \
wenzelm@27478
    27
  HOL-NSA \
wenzelm@23443
    28
  HOL-Nominal-Examples \
haftmann@32633
    29
  HOL-Number_Theory \
haftmann@32633
    30
  HOL-Old_Number_Theory \
wenzelm@37976
    31
  HOL-Predicate_Compile_Examples \
wenzelm@34237
    32
  HOL-Proofs-Extraction \
wenzelm@34237
    33
  HOL-Proofs-Lambda \
wenzelm@33028
    34
  HOL-SET_Protocol \
kleing@22410
    35
  HOL-UNITY \
wenzelm@27478
    36
  HOL-Word \
wenzelm@37976
    37
  HOL-Word-SMT_Examples \
kleing@22410
    38
  HOL-ex \
wenzelm@30616
    39
  HOLCF \
wenzelm@30616
    40
  IOA \
kleing@22410
    41
  ZF \
wenzelm@29283
    42
  ZF-Constructible \
kleing@22410
    43
  ZF-UNITY"
kleing@22410
    44
wenzelm@24831
    45
AFP_SESSIONS="\
wenzelm@37976
    46
  Coinductive \
wenzelm@29283
    47
  CoreC++ \
wenzelm@37976
    48
  Group-Ring-Module \
wenzelm@37976
    49
  Group-Ring-Module-Valuation \
wenzelm@29283
    50
  HOL-BytecodeLogicJmlTypes \
wenzelm@37976
    51
  HOL-Collections \
wenzelm@29283
    52
  HOL-DiskPaxos \
wenzelm@37976
    53
  HOL-FeatherweightJava \
wenzelm@29283
    54
  HOL-Fermat3_4 \
wenzelm@29283
    55
  HOL-Flyspeck-Tame \
wenzelm@37976
    56
  HOL-Free-Groups \
wenzelm@37976
    57
  HOL-GraphMarkingIBP \
wenzelm@29283
    58
  HOL-JiveDataStoreModel \
wenzelm@37976
    59
  HOL-Locally-Nameless-Sigma \
wenzelm@37976
    60
  HOL-Ordinals_and_Cardinals \
wenzelm@29283
    61
  HOL-POPLmark-deBruijn \
wenzelm@37976
    62
  HOL-Presburger-Automata \
wenzelm@29283
    63
  HOL-Program-Conflict-Analysis \
wenzelm@29283
    64
  HOL-RSAPSS \
wenzelm@29283
    65
  HOL-Recursion-Theory-I \
wenzelm@29283
    66
  HOL-SATSolverVerification \
wenzelm@29283
    67
  HOL-SIFPL \
wenzelm@29283
    68
  HOL-SenSocialChoice \
wenzelm@29283
    69
  HOL-SumSquares \
wenzelm@29283
    70
  HOL-Topology \
wenzelm@37976
    71
  HOL-Tree-Automata \
wenzelm@37976
    72
  HOL-Word-JinjaThreads \
wenzelm@37976
    73
  HOLCF-WorkerWrapper \
wenzelm@37976
    74
  HRB-Slicing \
wenzelm@37976
    75
  Jinja \
wenzelm@37976
    76
  Jinja-Slicing \
wenzelm@29283
    77
  LinearQuantifierElim \
wenzelm@29283
    78
  Simpl \
wenzelm@37976
    79
  Simpl-BDD \
wenzelm@37976
    80
  Slicing \
wenzelm@37976
    81
  Slicing-InformationFlowSlicing"
wenzelm@24831
    82
kleing@22410
    83
for PLATFORM in $PLATFORMS
kleing@22410
    84
do
wenzelm@24831
    85
  if [ "$PLATFORM" = afp ]; then
wenzelm@24831
    86
    SESSIONS="$AFP_SESSIONS"
wenzelm@24831
    87
  else
wenzelm@24831
    88
    SESSIONS="$ISABELLE_SESSIONS"
wenzelm@24831
    89
  fi
wenzelm@24831
    90
kleing@22410
    91
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
kleing@22410
    92
  cat > "stats/$PLATFORM.html" <<EOF
kleing@22410
    93
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
kleing@22410
    94
<html>
kleing@22410
    95
<head><title>Development Snapshot -- Performance Statistics</title></head>
kleing@22410
    96
kleing@22410
    97
<body>
kleing@22410
    98
<h1>$PLATFORM</h1>
kleing@22410
    99
EOF
kleing@22410
   100
kleing@22410
   101
for SESSION in $SESSIONS
kleing@22410
   102
do
kleing@22410
   103
  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
kleing@22410
   104
done
kleing@22410
   105
kleing@22410
   106
echo "</body>" >> "stats/$PLATFORM.html"
kleing@22410
   107
echo "</html>" >> "stats/$PLATFORM.html"
kleing@22410
   108
kleing@22410
   109
done