Admin/isatest/isatest-stats
author wenzelm
Wed, 27 Mar 2013 21:07:10 +0100
changeset 51562 5fffa75d2432
parent 51059 c6a74742f8fe
child 52283 1ce9feb47535
permissions -rwxr-xr-x
separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
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
51562
5fffa75d2432 separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
wenzelm
parents: 51059
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-poly-M8-skip_proofs 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-Algebra
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    14
  HOL-Auth
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    15
  HOL-BNF
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    16
  HOL-BNF-Examples
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    17
  HOL-BNF-LFP
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    18
  HOL-Bali
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    19
  HOL-Boogie
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    20
  HOL-Boogie-Examples
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    21
  HOL-Cardinals
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    22
  HOL-Cardinals-Base
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    23
  HOL-Codegenerator_Test
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    24
  HOL-Datatype_Benchmark
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    25
  HOL-Decision_Procs
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    26
  HOL-Hahn_Banach
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    27
  HOL-Hoare
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    28
  HOL-Hoare_Parallel
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    29
  HOL-IMP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    30
  HOL-IMPP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    31
  HOL-IOA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    32
  HOL-Imperative_HOL
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    33
  HOL-Import
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    34
  HOL-Induct
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    35
  HOL-Isar_Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    36
  HOL-Lattice
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    37
  HOL-Library
46988
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46651
diff changeset
    38
  HOL-Matrix_LP
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    39
  HOL-Metis_Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    40
  HOL-MicroJava
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    41
  HOL-MicroJava-skip_proofs
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    42
  HOL-Mirabelle
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    43
  HOL-Mirabelle-ex
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    44
  HOL-Multivariate_Analysis
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    45
  HOL-Mutabelle
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    46
  HOL-NSA
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    47
  HOL-NSA-Examples
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    48
  HOL-NanoJava
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    49
  HOL-Nitpick_Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    50
  HOL-Nominal
45142
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance;
wenzelm
parents: 44993
diff changeset
    51
  HOL-Nominal-Examples
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    52
  HOL-Number_Theory
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    53
  HOL-Old_Number_Theory
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    54
  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
    55
  HOL-Probability
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    56
  HOL-Prolog
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    57
  HOL-Proofs
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    58
  HOL-Proofs-Extraction
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    59
  HOL-Proofs-Lambda
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    60
  HOL-Proofs-ex
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    61
  HOL-Quickcheck_Benchmark
46651
1258eab48270 updated stats according to src/HOL/IsaMakefile;
wenzelm
parents: 45888
diff changeset
    62
  HOL-Quickcheck_Examples
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    63
  HOL-Quotient_Examples
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    64
  HOL-Record_Benchmark
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    65
  HOL-SET_Protocol
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    66
  HOL-SPARK
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    67
  HOL-SPARK-Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    68
  HOL-SPARK-Manual
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    69
  HOL-Statespace
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    70
  HOL-TLA
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    71
  HOL-TLA-Buffer
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    72
  HOL-TLA-Inc
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    73
  HOL-TLA-Memory
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    74
  HOL-TPTP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    75
  HOL-UNITY
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    76
  HOL-Unix
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    77
  HOL-Word
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    78
  HOL-Word-Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    79
  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
    80
  HOL-ZF
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    81
  HOL-ex
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    82
  HOLCF
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    83
  HOLCF-FOCUS
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    84
  HOLCF-IMP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    85
  HOLCF-Library
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    86
  HOLCF-Tutorial
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    87
  HOLCF-ex
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    88
  IOA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    89
  IOA-ABP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    90
  IOA-NTP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    91
  IOA-Storage
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
    92
  IOA-ex
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    93
  ZF
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    94
  ZF-AC
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    95
  ZF-Coind
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    96
  ZF-Constructible
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    97
  ZF-IMP
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    98
  ZF-Induct
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
    99
  ZF-Resid
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   100
  ZF-UNITY
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   101
  ZF-ex
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   102
"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   103
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   104
AFP_SESSIONS="
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   105
  AVL-Trees
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   106
  Abortable_Linearizable_Modules
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   107
  Abstract-Hoare-Logics
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   108
  Abstract-Rewriting
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   109
  ArrowImpossibilityGS
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   110
  AutoFocus-Stream
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   111
  BDD
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   112
  BinarySearchTree
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   113
  Binomial-Heaps
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   114
  Binomial-Queues
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   115
  Bondy
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   116
  BytecodeLogicJmlTypes
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   117
  CCS
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   118
  Category
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   119
  Category2
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   120
  Cauchy
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   121
  Circus
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   122
  ClockSynchInst
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   123
  CofGroups
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   124
  Coinductive
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   125
  Collections
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   126
  Compiling-Exceptions-Correctly
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   127
  Completeness
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   128
  CoreC++
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   129
  DPT-SAT-Solver
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   130
  DataRefinementIBP
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   131
  Datatype_Order_Generator
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   132
  Depth-First-Search
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   133
  Dijkstra_Shortest_Path
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   134
  DiskPaxos
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   135
  Efficient-Mergesort
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   136
  Example-Submission
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   137
  FFT
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   138
  FOL-Fitting
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   139
  FeatherweightJava
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   140
  Fermat3_4
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   141
  FileRefinement
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   142
  FinFun
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   143
  Finger-Trees
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   144
  Flyspeck-Tame
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   145
  Free-Boolean-Algebra
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   146
  Free-Groups
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   147
  FunWithFunctions
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   148
  FunWithTilings
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   149
  Functional-Automata
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   150
  Gauss-Jordan-Elim-Fun
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   151
  GenClock
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   152
  General-Triangle
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   153
  Girth_Chromatic
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   154
  GraphMarkingIBP
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   155
  Group-Ring-Module
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   156
  HRB-Slicing
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   157
  Heard_Of
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   158
  HotelKeyCards
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   159
  Huffman
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   160
  Impossible_Geometry
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   161
  Inductive_Confidentiality
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   162
  InformationFlowSlicing_Inter
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   163
  InformationFlowSlicing_Intra
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   164
  Integration
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   165
  Jinja
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   166
  JinjaThreads
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   167
  JiveDataStoreModel
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   168
  KBPs
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   169
  Kleene_Algebra
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   170
  Lam-ml-Normalization
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   171
  LatticeProperties
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   172
  Lazy-Lists-II
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   173
  LightweightJava
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   174
  LinearQuantifierElim
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   175
  List-Index
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   176
  List-Infinite
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   177
  Locally-Nameless-Sigma
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   178
  Lower_Semicontinuous
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   179
  Markov_Models
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   180
  Marriage
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   181
  Matrix
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   182
  Max-Card-Matching
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   183
  MiniML
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   184
  MonoBoolTranAlgebra
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   185
  MuchAdoAboutTwo
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   186
  Myhill-Nerode
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   187
  Nat-Interval-Logic
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   188
  NormByEval
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   189
  Open_Induction
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   190
  Ordinal
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   191
  Ordinals_and_Cardinals
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   192
  Ordinary_Differential_Equations
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   193
  PCF
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   194
  POPLmark-deBruijn
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   195
  Perfect-Number-Thm
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   196
  Pi_Calculus
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   197
  Polynomials
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   198
  Possibilistic_Noninterference
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   199
  Presburger-Automata
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   200
  Program-Conflict-Analysis
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   201
  PseudoHoops
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   202
  Psi_Calculi
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   203
  RIPEMD-160-SPARK
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   204
  RSAPSS
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   205
  Ramsey-Infinite
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   206
  Rank_Nullity_Theorem
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   207
  Recursion-Theory-I
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   208
  Refine_Monadic
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   209
  Regular-Sets
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   210
  Robbins-Conjecture
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   211
  SATSolverVerification
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   212
  SIFPL
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   213
  SenSocialChoice
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   214
  Separation_Algebra
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   215
  Separation_Logic_Imperative_HOL
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   216
  SequentInvertibility
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   217
  Shivers-CFA
45194
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   218
  Simpl
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277);
wenzelm
parents: 45142
diff changeset
   219
  Slicing
51059
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   220
  Sqrt_Babylonian
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   221
  Statecharts
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   222
  Stream-Fusion
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   223
  Stuttering_Equivalence
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   224
  SumSquares
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   225
  TLA
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   226
  Tarskis_Geometry
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   227
  Topology
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   228
  Transitive-Closure
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   229
  Transitive-Closure-II
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   230
  Tree-Automata
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   231
  Tycon
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   232
  Valuation
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   233
  Verified-Prover
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   234
  VolpanoSmith
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   235
  Well_Quasi_Orders
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   236
  WorkerWrapper
c6a74742f8fe manual update of sessions, based on "isabelle build -nvc";
wenzelm
parents: 49938
diff changeset
   237
"
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   238
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   239
for PLATFORM in $PLATFORMS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   240
do
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   241
  if [ "$PLATFORM" = afp ]; then
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   242
    SESSIONS="$AFP_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   243
  else
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   244
    SESSIONS="$ISABELLE_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   245
  fi
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 24489
diff changeset
   246
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   247
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   248
  cat > "stats/$PLATFORM.html" <<EOF
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   249
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   250
<html>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   251
<head><title>Development Snapshot -- Performance Statistics</title></head>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   252
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   253
<body>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   254
<h1>$PLATFORM</h1>
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   255
EOF
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   256
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   257
for SESSION in $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   258
do
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   259
  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
   260
done
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   261
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   262
echo "</body>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   263
echo "</html>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   264
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   265
done