Admin/isatest/isatest-stats
author wenzelm
Thu, 11 Aug 2011 12:53:41 +0200
changeset 44152 a07748619f53
parent 42461 56975de9e341
child 44993 9a2d100dd3eb
permissions -rwxr-xr-x
somewhat more uniform THIS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     1
#!/usr/bin/env bash
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     2
#
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     3
# Author: Makarius
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     4
#
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     5
# DESCRIPTION: Standard statistics.
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     6
44152
a07748619f53 somewhat more uniform THIS;
wenzelm
parents: 42461
diff changeset
     7
THIS="$(cd "$(dirname "$0")"; pwd)"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     8
42461
56975de9e341 stats for mac-poly-M2;
wenzelm
parents: 41646
diff changeset
     9
PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    10
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    11
ISABELLE_SESSIONS="\
27448
28914fe628c8 moved HOL-Plain up;
wenzelm
parents: 27429
diff changeset
    12
  HOL-Plain \
28530
843b35caa8c4 added HOL-Main;
wenzelm
parents: 27478
diff changeset
    13
  HOL-Main \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    14
  HOL \
34237
225daff4323b updated stats;
wenzelm
parents: 33264
diff changeset
    15
  HOL-Proofs \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    16
  HOL-Library \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    17
  HOL-Algebra \
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    18
  HOL-Auth \
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    19
  HOL-Bali \
30111
01a87bc13415 include HOL-Decision_Procs in stats;
wenzelm
parents: 29283
diff changeset
    20
  HOL-Decision_Procs \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    21
  HOL-Hoare \
33072
ae416aebbb75 updated session name;
wenzelm
parents: 33028
diff changeset
    22
  HOL-Hoare_Parallel \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    23
  HOL-Imperative_HOL \
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 32633
diff changeset
    24
  HOL-Metis_Examples \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    25
  HOL-MicroJava \
34237
225daff4323b updated stats;
wenzelm
parents: 33264
diff changeset
    26
  HOL-Multivariate_Analysis \
27478
ac3b0f881d89 more sessions;
wenzelm
parents: 27448
diff changeset
    27
  HOL-NSA \
23443
fd8ffc8a5709 added HOL-Nominal-Examples;
wenzelm
parents: 22410
diff changeset
    28
  HOL-Nominal-Examples \
32633
4ba4bfa08749 adjusted to new Number Theory scenario
haftmann
parents: 32421
diff changeset
    29
  HOL-Number_Theory \
4ba4bfa08749 adjusted to new Number Theory scenario
haftmann
parents: 32421
diff changeset
    30
  HOL-Old_Number_Theory \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    31
  HOL-Predicate_Compile_Examples \
34237
225daff4323b updated stats;
wenzelm
parents: 33264
diff changeset
    32
  HOL-Proofs-Extraction \
225daff4323b updated stats;
wenzelm
parents: 33264
diff changeset
    33
  HOL-Proofs-Lambda \
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
    34
  HOL-SET_Protocol \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    35
  HOL-UNITY \
27478
ac3b0f881d89 more sessions;
wenzelm
parents: 27448
diff changeset
    36
  HOL-Word \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    37
  HOL-Word-SMT_Examples \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    38
  HOL-ex \
30616
ac79f1bb5db3 more stats;
wenzelm
parents: 30111
diff changeset
    39
  HOLCF \
ac79f1bb5db3 more stats;
wenzelm
parents: 30111
diff changeset
    40
  IOA \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    41
  ZF \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    42
  ZF-Constructible \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    43
  ZF-UNITY"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    44
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    45
AFP_SESSIONS="\
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    46
  Coinductive \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    47
  CoreC++ \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    48
  Group-Ring-Module \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    49
  Group-Ring-Module-Valuation \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    50
  HOL-BytecodeLogicJmlTypes \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    51
  HOL-Collections \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    52
  HOL-DiskPaxos \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    53
  HOL-FeatherweightJava \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    54
  HOL-Fermat3_4 \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    55
  HOL-Flyspeck-Tame \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    56
  HOL-Free-Groups \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    57
  HOL-GraphMarkingIBP \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    58
  HOL-JiveDataStoreModel \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    59
  HOL-Locally-Nameless-Sigma \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    60
  HOL-Ordinals_and_Cardinals \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    61
  HOL-POPLmark-deBruijn \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    62
  HOL-Presburger-Automata \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    63
  HOL-Program-Conflict-Analysis \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    64
  HOL-RSAPSS \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    65
  HOL-Recursion-Theory-I \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    66
  HOL-SATSolverVerification \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    67
  HOL-SIFPL \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    68
  HOL-SenSocialChoice \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    69
  HOL-SumSquares \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    70
  HOL-Topology \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    71
  HOL-Tree-Automata \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    72
  HOL-Word-JinjaThreads \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    73
  HOLCF-WorkerWrapper \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    74
  HRB-Slicing \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    75
  Jinja \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    76
  Jinja-Slicing \
29283
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    77
  LinearQuantifierElim \
f4743512b12d updated sessions;
wenzelm
parents: 28602
diff changeset
    78
  Simpl \
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    79
  Simpl-BDD \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    80
  Slicing \
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    81
  Slicing-InformationFlowSlicing"
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    82
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    83
for PLATFORM in $PLATFORMS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    84
do
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    85
  if [ "$PLATFORM" = afp ]; then
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    86
    SESSIONS="$AFP_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    87
  else
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    88
    SESSIONS="$ISABELLE_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    89
  fi
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    90
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    91
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    92
  cat > "stats/$PLATFORM.html" <<EOF
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    93
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    94
<html>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    95
<head><title>Development Snapshot -- Performance Statistics</title></head>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    96
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    97
<body>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    98
<h1>$PLATFORM</h1>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    99
EOF
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   100
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   101
for SESSION in $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   102
do
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   103
  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   104
done
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   105
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   106
echo "</body>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   107
echo "</html>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   108
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   109
done