Admin/isatest/isatest-stats
author wenzelm
Fri Oct 14 11:34:30 2011 +0200 (2011-10-14)
changeset 45142 97e81a8aa277
parent 44993 9a2d100dd3eb
child 45194 d825a8f1d088
permissions -rwxr-xr-x
more complete stats, including small sessions which provide some clues on main HOL baseline performance;
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="\
kleing@22410
    12
  HOL-Auth \
kleing@22410
    13
  HOL-Bali \
wenzelm@45142
    14
  HOL-Boogie-Examples \
wenzelm@30111
    15
  HOL-Decision_Procs \
wenzelm@45142
    16
  HOL-Hahn_Banach \
kleing@22410
    17
  HOL-Hoare \
wenzelm@33072
    18
  HOL-Hoare_Parallel \
wenzelm@45142
    19
  HOL-IMPP \
wenzelm@45142
    20
  HOL-IOA \
wenzelm@37976
    21
  HOL-Imperative_HOL \
wenzelm@45142
    22
  HOL-Import \
wenzelm@45142
    23
  HOL-Induct \
wenzelm@45142
    24
  HOL-Isar_Examples \
wenzelm@45142
    25
  HOL-Lattice \
wenzelm@45142
    26
  HOL-Library-Codegenerator_Test \
wenzelm@45142
    27
  HOL-Matrix \
wenzelm@33027
    28
  HOL-Metis_Examples \
kleing@22410
    29
  HOL-MicroJava \
wenzelm@45142
    30
  HOL-Mirabelle \
wenzelm@45142
    31
  HOL-Mutabelle \
wenzelm@45142
    32
  HOL-NanoJava \
wenzelm@45142
    33
  HOL-Nitpick_Examples \
wenzelm@45142
    34
  HOL-Nominal-Examples
haftmann@32633
    35
  HOL-Number_Theory \
haftmann@32633
    36
  HOL-Old_Number_Theory \
wenzelm@37976
    37
  HOL-Predicate_Compile_Examples \
wenzelm@45142
    38
  HOL-Probability
wenzelm@45142
    39
  HOL-Prolog \
wenzelm@34237
    40
  HOL-Proofs-Extraction \
wenzelm@34237
    41
  HOL-Proofs-Lambda \
wenzelm@45142
    42
  HOL-Proofs-ex \
wenzelm@45142
    43
  HOL-Quotient_Examples \
wenzelm@33028
    44
  HOL-SET_Protocol \
wenzelm@45142
    45
  HOL-SPARK-Examples \
wenzelm@45142
    46
  HOL-SPARK-Manual \
wenzelm@45142
    47
  HOL-Statespace \
wenzelm@45142
    48
  HOL-TPTP \
kleing@22410
    49
  HOL-UNITY \
wenzelm@45142
    50
  HOL-Unix \
wenzelm@45142
    51
  HOL-Word-Examples \
wenzelm@37976
    52
  HOL-Word-SMT_Examples \
wenzelm@45142
    53
  HOL-ZF
kleing@22410
    54
  HOL-ex \
wenzelm@45142
    55
  HOLCF-FOCUS \
wenzelm@45142
    56
  HOLCF-IMP \
wenzelm@45142
    57
  HOLCF-Library \
wenzelm@45142
    58
  HOLCF-Tutorial \
wenzelm@45142
    59
  HOLCF-ex \
wenzelm@45142
    60
  IOA-ABP \
wenzelm@45142
    61
  IOA-NTP \
wenzelm@45142
    62
  IOA-Storage \
wenzelm@45142
    63
  IOA-ex \
wenzelm@45142
    64
  TLA-Buffer \
wenzelm@45142
    65
  TLA-Inc \
wenzelm@45142
    66
  TLA-Memory"
kleing@22410
    67
wenzelm@24831
    68
AFP_SESSIONS="\
wenzelm@45142
    69
  ArrowImpossibilityGS \
wenzelm@37976
    70
  Coinductive \
wenzelm@29283
    71
  CoreC++ \
wenzelm@45142
    72
  HOL-AVL-Trees \
wenzelm@45142
    73
  HOL-Abstract-Hoare-Logics \
wenzelm@45142
    74
  HOL-Abstract-Rewriting \
wenzelm@45142
    75
  HOL-BinarySearchTree \
wenzelm@45142
    76
  HOL-Binomial-Heaps \
wenzelm@45142
    77
  HOL-Binomial-Queues \
wenzelm@29283
    78
  HOL-BytecodeLogicJmlTypes \
wenzelm@45142
    79
  HOL-Category \
wenzelm@45142
    80
  HOL-Category2 \
wenzelm@45142
    81
  HOL-Cauchy \
wenzelm@45142
    82
  HOL-ClockSynchInst \
wenzelm@45142
    83
  HOL-CofGroups \
wenzelm@37976
    84
  HOL-Collections \
wenzelm@45142
    85
  HOL-Compiling-Exceptions-Correctly \
wenzelm@45142
    86
  HOL-Completeness \
wenzelm@45142
    87
  HOL-DPT-SAT-Solver \
wenzelm@45142
    88
  HOL-DataRefinementIBP \
wenzelm@45142
    89
  HOL-Depth-First-Search \
wenzelm@29283
    90
  HOL-DiskPaxos \
wenzelm@45142
    91
  HOL-Example-Submission \
wenzelm@45142
    92
  HOL-FFT \
wenzelm@45142
    93
  HOL-FOL-Fitting \
wenzelm@37976
    94
  HOL-FeatherweightJava \
wenzelm@45142
    95
  HOL-FileRefinement \
wenzelm@45142
    96
  HOL-FinFun \
wenzelm@45142
    97
  HOL-Finger-Trees \
wenzelm@29283
    98
  HOL-Flyspeck-Tame \
wenzelm@45142
    99
  HOL-Free-Boolean-Algebra \
wenzelm@37976
   100
  HOL-Free-Groups \
wenzelm@45142
   101
  HOL-FunWithFunctions \
wenzelm@45142
   102
  HOL-FunWithTilings \
wenzelm@45142
   103
  HOL-Functional-Automata \
wenzelm@45142
   104
  HOL-Gauss-Jordan-Elim-Fun \
wenzelm@45142
   105
  HOL-GenClock \
wenzelm@45142
   106
  HOL-General-Triangle \
wenzelm@37976
   107
  HOL-GraphMarkingIBP \
wenzelm@45142
   108
  HOL-HotelKeyCards \
wenzelm@45142
   109
  HOL-Huffman \
wenzelm@45142
   110
  HOL-Integration \
wenzelm@29283
   111
  HOL-JiveDataStoreModel \
wenzelm@45142
   112
  HOL-KBPs \
wenzelm@45142
   113
  HOL-Lazy-Lists-II \
wenzelm@45142
   114
  HOL-LightweightJava \
wenzelm@45142
   115
  HOL-List-Index \
wenzelm@37976
   116
  HOL-Locally-Nameless-Sigma \
wenzelm@45142
   117
  HOL-Marriage \
wenzelm@45142
   118
  HOL-Matrix \
wenzelm@45142
   119
  HOL-Max-Card-Matching \
wenzelm@45142
   120
  HOL-MiniML \
wenzelm@45142
   121
  HOL-MuchAdoAboutTwo \
wenzelm@45142
   122
  HOL-Multivariate_Analysis \
wenzelm@45142
   123
  HOL-Myhill-Nerode \
wenzelm@45142
   124
  HOL-Nominal \
wenzelm@45142
   125
  HOL-Nominal-Lam-ml-Normalization \
wenzelm@45142
   126
  HOL-Nominal-SequentInvertibility \
wenzelm@45142
   127
  HOL-Ordinal \
wenzelm@37976
   128
  HOL-Ordinals_and_Cardinals \
wenzelm@29283
   129
  HOL-POPLmark-deBruijn \
wenzelm@45142
   130
  HOL-Perfect-Number-Thm \
wenzelm@45142
   131
  HOL-Polynomials \
wenzelm@37976
   132
  HOL-Presburger-Automata \
wenzelm@29283
   133
  HOL-Program-Conflict-Analysis \
wenzelm@45142
   134
  HOL-Ramsey-Infinite \
wenzelm@29283
   135
  HOL-Recursion-Theory-I \
wenzelm@45142
   136
  HOL-Regular-Sets \
wenzelm@45142
   137
  HOL-Robbins-Conjecture \
wenzelm@29283
   138
  HOL-SATSolverVerification \
wenzelm@29283
   139
  HOL-SIFPL \
wenzelm@29283
   140
  HOL-SenSocialChoice \
wenzelm@45142
   141
  HOL-Statecharts \
wenzelm@29283
   142
  HOL-Topology \
wenzelm@45142
   143
  HOL-Transitive-Closure \
wenzelm@37976
   144
  HOL-Tree-Automata \
wenzelm@45142
   145
  HOL-Verified-Prover \
wenzelm@45142
   146
  HOL-Word \
wenzelm@45142
   147
  HOL-Word-RIPEMD-160-SPARK \
wenzelm@45142
   148
  HOLCF \
wenzelm@45142
   149
  HOLCF-Shivers-CFA \
wenzelm@45142
   150
  HOLCF-Stream-Fusion \
wenzelm@37976
   151
  HOLCF-WorkerWrapper \
wenzelm@37976
   152
  HRB-Slicing \
wenzelm@45142
   153
  HRB-Slicing-InformationFlowSlicing \
wenzelm@37976
   154
  Jinja \
wenzelm@45142
   155
  Jinja \
wenzelm@45142
   156
  LatticeProperties \
wenzelm@45142
   157
  LatticeProperties-MonoBoolTranAlgebra \
wenzelm@45142
   158
  LatticeProperties-PseudoHoops \
wenzelm@45142
   159
  Lower_Semicontinuous \
wenzelm@45142
   160
  NormByEval \
wenzelm@29283
   161
  Simpl \
wenzelm@37976
   162
  Simpl-BDD \
wenzelm@37976
   163
  Slicing \
wenzelm@45142
   164
  Slicing \
wenzelm@45142
   165
  Slicing-InformationFlowSlicing \
wenzelm@45142
   166
  VolpanoSmith"
wenzelm@45142
   167
wenzelm@24831
   168
kleing@22410
   169
for PLATFORM in $PLATFORMS
kleing@22410
   170
do
wenzelm@24831
   171
  if [ "$PLATFORM" = afp ]; then
wenzelm@24831
   172
    SESSIONS="$AFP_SESSIONS"
wenzelm@24831
   173
  else
wenzelm@24831
   174
    SESSIONS="$ISABELLE_SESSIONS"
wenzelm@24831
   175
  fi
wenzelm@24831
   176
kleing@22410
   177
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
kleing@22410
   178
  cat > "stats/$PLATFORM.html" <<EOF
kleing@22410
   179
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
kleing@22410
   180
<html>
kleing@22410
   181
<head><title>Development Snapshot -- Performance Statistics</title></head>
kleing@22410
   182
kleing@22410
   183
<body>
kleing@22410
   184
<h1>$PLATFORM</h1>
kleing@22410
   185
EOF
kleing@22410
   186
kleing@22410
   187
for SESSION in $SESSIONS
kleing@22410
   188
do
kleing@22410
   189
  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
kleing@22410
   190
done
kleing@22410
   191
kleing@22410
   192
echo "</body>" >> "stats/$PLATFORM.html"
kleing@22410
   193
echo "</html>" >> "stats/$PLATFORM.html"
kleing@22410
   194
kleing@22410
   195
done