Admin/isatest/isatest-stats
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 49938 1c06f8d244af
child 51059 c6a74742f8fe
permissions -rwxr-xr-x
tuned;
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
49938
1c06f8d244af ignore old stuff and thus speed up the script greatly;
wenzelm
parents: 49310
diff changeset
     9
PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-sml-dev"
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
    10
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    11
ISABELLE_SESSIONS="
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    12
  HOL
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    13
  HOL-Main
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    14
  HOL-Plain
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    15
  HOL-Base
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    16
  HOL-Library
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    17
  HOL-Algebra
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    18
  HOL-Auth
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    19
  HOL-Bali
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    20
  HOL-Boogie
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    21
  HOL-Boogie-Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    22
  HOL-Decision_Procs
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    23
  HOL-Hahn_Banach
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    24
  HOL-Hoare
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    25
  HOL-Hoare_Parallel
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    26
  HOL-IMP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    27
  HOL-IMPP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    28
  HOL-IOA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    29
  HOL-Imperative_HOL
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    30
  HOL-Import
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    31
  HOL-Induct
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    32
  HOL-Isar_Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    33
  HOL-Lattice
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    34
  HOL-Library-Codegenerator_Test
46988
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46651
diff changeset
    35
  HOL-Matrix_LP
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    36
  HOL-Metis_Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    37
  HOL-MicroJava
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    38
  HOL-Mirabelle
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    39
  HOL-Multivariate_Analysis
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    40
  HOL-Mutabelle
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    41
  HOL-NSA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    42
  HOL-NanoJava
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    43
  HOL-Nitpick_Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    44
  HOL-Nominal
45142
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance;
wenzelm
parents: 44993
diff changeset
    45
  HOL-Nominal-Examples
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    46
  HOL-Number_Theory
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    47
  HOL-Old_Number_Theory
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    48
  HOL-Predicate_Compile_Examples
45142
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance;
wenzelm
parents: 44993
diff changeset
    49
  HOL-Probability
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    50
  HOL-Prolog
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    51
  HOL-Proofs
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    52
  HOL-Proofs-Extraction
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    53
  HOL-Proofs-Lambda
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    54
  HOL-Proofs-ex
46651
1258eab48270 updated stats according to src/HOL/IsaMakefile;
wenzelm
parents: 45888
diff changeset
    55
  HOL-Quickcheck_Examples
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    56
  HOL-Quotient_Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    57
  HOL-SET_Protocol
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    58
  HOL-SPARK
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    59
  HOL-SPARK-Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    60
  HOL-SPARK-Manual
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    61
  HOL-Statespace
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    62
  HOL-TPTP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    63
  HOL-UNITY
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    64
  HOL-Unix
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    65
  HOL-Word
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    66
  HOL-Word-Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    67
  HOL-Word-SMT_Examples
45142
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance;
wenzelm
parents: 44993
diff changeset
    68
  HOL-ZF
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    69
  HOL-ex
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    70
  HOL4
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    71
  HOLCF
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    72
  HOLCF-FOCUS
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    73
  HOLCF-IMP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    74
  HOLCF-Library
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    75
  HOLCF-Tutorial
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    76
  HOLCF-ex
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    77
  IOA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    78
  IOA-ABP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    79
  IOA-NTP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    80
  IOA-Storage
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    81
  IOA-ex
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    82
  TLA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    83
  TLA-Buffer
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    84
  TLA-Inc
45888
66b419de5f38 more stats;
wenzelm
parents: 45194
diff changeset
    85
  TLA-Memory
66b419de5f38 more stats;
wenzelm
parents: 45194
diff changeset
    86
  HOL-Datatype_Benchmark
66b419de5f38 more stats;
wenzelm
parents: 45194
diff changeset
    87
  HOL-Record_Benchmark"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    88
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    89
AFP_SESSIONS="
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    90
  ArrowImpossibilityGS
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    91
  Coinductive
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    92
  CoreC++
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    93
  HOL-AVL-Trees
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    94
  HOL-Abstract-Hoare-Logics
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    95
  HOL-Abstract-Rewriting
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    96
  HOL-BinarySearchTree
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    97
  HOL-Binomial-Heaps
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    98
  HOL-Binomial-Queues
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    99
  HOL-BytecodeLogicJmlTypes
49310
6e30078de4f0 renamed "Ordinals_and_Cardinals" to "Cardinals"
blanchet
parents: 47044
diff changeset
   100
  HOL-Cardinals
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   101
  HOL-Category
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   102
  HOL-Category2
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   103
  HOL-Cauchy
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   104
  HOL-ClockSynchInst
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   105
  HOL-CofGroups
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   106
  HOL-Collections
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   107
  HOL-Compiling-Exceptions-Correctly
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   108
  HOL-Completeness
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   109
  HOL-DPT-SAT-Solver
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   110
  HOL-DataRefinementIBP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   111
  HOL-Depth-First-Search
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   112
  HOL-DiskPaxos
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   113
  HOL-Example-Submission
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   114
  HOL-FFT
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   115
  HOL-FOL-Fitting
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   116
  HOL-FeatherweightJava
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   117
  HOL-FileRefinement
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   118
  HOL-FinFun
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   119
  HOL-Finger-Trees
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   120
  HOL-Flyspeck-Tame
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   121
  HOL-Free-Boolean-Algebra
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   122
  HOL-Free-Groups
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   123
  HOL-FunWithFunctions
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   124
  HOL-FunWithTilings
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   125
  HOL-Functional-Automata
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   126
  HOL-Gauss-Jordan-Elim-Fun
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   127
  HOL-GenClock
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   128
  HOL-General-Triangle
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   129
  HOL-GraphMarkingIBP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   130
  HOL-HotelKeyCards
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   131
  HOL-Huffman
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   132
  HOL-Integration
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   133
  HOL-JiveDataStoreModel
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   134
  HOL-KBPs
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   135
  HOL-Lazy-Lists-II
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   136
  HOL-LightweightJava
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   137
  HOL-List-Index
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   138
  HOL-Locally-Nameless-Sigma
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   139
  HOL-Marriage
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   140
  HOL-Matrix
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   141
  HOL-Max-Card-Matching
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   142
  HOL-MiniML
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   143
  HOL-MuchAdoAboutTwo
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   144
  HOL-Multivariate_Analysis
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   145
  HOL-Myhill-Nerode
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   146
  HOL-Nominal
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   147
  HOL-Nominal-Lam-ml-Normalization
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   148
  HOL-Nominal-SequentInvertibility
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   149
  HOL-Ordinal
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   150
  HOL-POPLmark-deBruijn
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   151
  HOL-Perfect-Number-Thm
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   152
  HOL-Polynomials
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   153
  HOL-Presburger-Automata
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   154
  HOL-Program-Conflict-Analysis
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   155
  HOL-Ramsey-Infinite
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   156
  HOL-Recursion-Theory-I
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   157
  HOL-Regular-Sets
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   158
  HOL-Robbins-Conjecture
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   159
  HOL-SATSolverVerification
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   160
  HOL-SIFPL
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   161
  HOL-SenSocialChoice
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   162
  HOL-Statecharts
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   163
  HOL-Topology
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   164
  HOL-Transitive-Closure
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   165
  HOL-Tree-Automata
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   166
  HOL-Verified-Prover
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   167
  HOL-Word
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   168
  HOL-Word-RIPEMD-160-SPARK
47044
1ab41ea5b1c6 more stats;
wenzelm
parents: 46988
diff changeset
   169
  HOL-Word-JinjaThreads-Basic-JinjaThreads
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   170
  HOLCF
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   171
  HOLCF-Shivers-CFA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   172
  HOLCF-Stream-Fusion
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   173
  HOLCF-WorkerWrapper
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   174
  HRB-Slicing
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   175
  HRB-Slicing-InformationFlowSlicing
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   176
  Jinja
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   177
  LatticeProperties
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   178
  LatticeProperties-MonoBoolTranAlgebra
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   179
  LatticeProperties-PseudoHoops
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   180
  Lower_Semicontinuous
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   181
  NormByEval
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   182
  Simpl
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   183
  Simpl-BDD
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   184
  Slicing
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   185
  Slicing-InformationFlowSlicing
45142
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance;
wenzelm
parents: 44993
diff changeset
   186
  VolpanoSmith"
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance;
wenzelm
parents: 44993
diff changeset
   187
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   188
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   189
for PLATFORM in $PLATFORMS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   190
do
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   191
  if [ "$PLATFORM" = afp ]; then
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   192
    SESSIONS="$AFP_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   193
  else
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   194
    SESSIONS="$ISABELLE_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   195
  fi
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   196
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   197
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   198
  cat > "stats/$PLATFORM.html" <<EOF
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   199
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   200
<html>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   201
<head><title>Development Snapshot -- Performance Statistics</title></head>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   202
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   203
<body>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   204
<h1>$PLATFORM</h1>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   205
EOF
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   206
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   207
for SESSION in $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   208
do
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   209
  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
   210
done
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   211
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   212
echo "</body>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   213
echo "</html>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   214
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   215
done