author | wenzelm |
Sat, 11 Aug 2012 21:32:46 +0200 | |
changeset 48775 | 92ceb058391f |
parent 47044 | 1ab41ea5b1c6 |
child 49310 | 6e30078de4f0 |
permissions | -rwxr-xr-x |
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 | 7 |
THIS="$(cd "$(dirname "$0")"; pwd)" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
8 |
|
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" |
24831
887d1b32a1a5
cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents:
24489
diff
changeset
|
10 |
|
45194 | 11 |
ISABELLE_SESSIONS=" |
12 |
HOL |
|
13 |
HOL-Main |
|
14 |
HOL-Plain |
|
15 |
HOL-Base |
|
16 |
HOL-Library |
|
17 |
HOL-Algebra |
|
18 |
HOL-Auth |
|
19 |
HOL-Bali |
|
20 |
HOL-Boogie |
|
21 |
HOL-Boogie-Examples |
|
22 |
HOL-Decision_Procs |
|
23 |
HOL-Hahn_Banach |
|
24 |
HOL-Hoare |
|
25 |
HOL-Hoare_Parallel |
|
26 |
HOL-IMP |
|
27 |
HOL-IMPP |
|
28 |
HOL-IOA |
|
29 |
HOL-Imperative_HOL |
|
30 |
HOL-Import |
|
31 |
HOL-Induct |
|
32 |
HOL-Isar_Examples |
|
33 |
HOL-Lattice |
|
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 | 36 |
HOL-Metis_Examples |
37 |
HOL-MicroJava |
|
38 |
HOL-Mirabelle |
|
39 |
HOL-Multivariate_Analysis |
|
40 |
HOL-Mutabelle |
|
41 |
HOL-NSA |
|
42 |
HOL-NanoJava |
|
43 |
HOL-Nitpick_Examples |
|
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 | 46 |
HOL-Number_Theory |
47 |
HOL-Old_Number_Theory |
|
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 | 50 |
HOL-Prolog |
51 |
HOL-Proofs |
|
52 |
HOL-Proofs-Extraction |
|
53 |
HOL-Proofs-Lambda |
|
54 |
HOL-Proofs-ex |
|
46651 | 55 |
HOL-Quickcheck_Examples |
45194 | 56 |
HOL-Quotient_Examples |
57 |
HOL-SET_Protocol |
|
58 |
HOL-SPARK |
|
59 |
HOL-SPARK-Examples |
|
60 |
HOL-SPARK-Manual |
|
61 |
HOL-Statespace |
|
62 |
HOL-TPTP |
|
63 |
HOL-UNITY |
|
64 |
HOL-Unix |
|
65 |
HOL-Word |
|
66 |
HOL-Word-Examples |
|
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 | 69 |
HOL-ex |
70 |
HOL4 |
|
71 |
HOLCF |
|
72 |
HOLCF-FOCUS |
|
73 |
HOLCF-IMP |
|
74 |
HOLCF-Library |
|
75 |
HOLCF-Tutorial |
|
76 |
HOLCF-ex |
|
77 |
IOA |
|
78 |
IOA-ABP |
|
79 |
IOA-NTP |
|
80 |
IOA-Storage |
|
81 |
IOA-ex |
|
82 |
TLA |
|
83 |
TLA-Buffer |
|
84 |
TLA-Inc |
|
45888 | 85 |
TLA-Memory |
86 |
HOL-Datatype_Benchmark |
|
87 |
HOL-Record_Benchmark" |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
88 |
|
45194 | 89 |
AFP_SESSIONS=" |
90 |
ArrowImpossibilityGS |
|
91 |
Coinductive |
|
92 |
CoreC++ |
|
93 |
HOL-AVL-Trees |
|
94 |
HOL-Abstract-Hoare-Logics |
|
95 |
HOL-Abstract-Rewriting |
|
96 |
HOL-BinarySearchTree |
|
97 |
HOL-Binomial-Heaps |
|
98 |
HOL-Binomial-Queues |
|
99 |
HOL-BytecodeLogicJmlTypes |
|
100 |
HOL-Category |
|
101 |
HOL-Category2 |
|
102 |
HOL-Cauchy |
|
103 |
HOL-ClockSynchInst |
|
104 |
HOL-CofGroups |
|
105 |
HOL-Collections |
|
106 |
HOL-Compiling-Exceptions-Correctly |
|
107 |
HOL-Completeness |
|
108 |
HOL-DPT-SAT-Solver |
|
109 |
HOL-DataRefinementIBP |
|
110 |
HOL-Depth-First-Search |
|
111 |
HOL-DiskPaxos |
|
112 |
HOL-Example-Submission |
|
113 |
HOL-FFT |
|
114 |
HOL-FOL-Fitting |
|
115 |
HOL-FeatherweightJava |
|
116 |
HOL-FileRefinement |
|
117 |
HOL-FinFun |
|
118 |
HOL-Finger-Trees |
|
119 |
HOL-Flyspeck-Tame |
|
120 |
HOL-Free-Boolean-Algebra |
|
121 |
HOL-Free-Groups |
|
122 |
HOL-FunWithFunctions |
|
123 |
HOL-FunWithTilings |
|
124 |
HOL-Functional-Automata |
|
125 |
HOL-Gauss-Jordan-Elim-Fun |
|
126 |
HOL-GenClock |
|
127 |
HOL-General-Triangle |
|
128 |
HOL-GraphMarkingIBP |
|
129 |
HOL-HotelKeyCards |
|
130 |
HOL-Huffman |
|
131 |
HOL-Integration |
|
132 |
HOL-JiveDataStoreModel |
|
133 |
HOL-KBPs |
|
134 |
HOL-Lazy-Lists-II |
|
135 |
HOL-LightweightJava |
|
136 |
HOL-List-Index |
|
137 |
HOL-Locally-Nameless-Sigma |
|
138 |
HOL-Marriage |
|
139 |
HOL-Matrix |
|
140 |
HOL-Max-Card-Matching |
|
141 |
HOL-MiniML |
|
142 |
HOL-MuchAdoAboutTwo |
|
143 |
HOL-Multivariate_Analysis |
|
144 |
HOL-Myhill-Nerode |
|
145 |
HOL-Nominal |
|
146 |
HOL-Nominal-Lam-ml-Normalization |
|
147 |
HOL-Nominal-SequentInvertibility |
|
148 |
HOL-Ordinal |
|
149 |
HOL-Ordinals_and_Cardinals |
|
150 |
HOL-POPLmark-deBruijn |
|
151 |
HOL-Perfect-Number-Thm |
|
152 |
HOL-Polynomials |
|
153 |
HOL-Presburger-Automata |
|
154 |
HOL-Program-Conflict-Analysis |
|
155 |
HOL-Ramsey-Infinite |
|
156 |
HOL-Recursion-Theory-I |
|
157 |
HOL-Regular-Sets |
|
158 |
HOL-Robbins-Conjecture |
|
159 |
HOL-SATSolverVerification |
|
160 |
HOL-SIFPL |
|
161 |
HOL-SenSocialChoice |
|
162 |
HOL-Statecharts |
|
163 |
HOL-Topology |
|
164 |
HOL-Transitive-Closure |
|
165 |
HOL-Tree-Automata |
|
166 |
HOL-Verified-Prover |
|
167 |
HOL-Word |
|
168 |
HOL-Word-RIPEMD-160-SPARK |
|
47044 | 169 |
HOL-Word-JinjaThreads-Basic-JinjaThreads |
45194 | 170 |
HOLCF |
171 |
HOLCF-Shivers-CFA |
|
172 |
HOLCF-Stream-Fusion |
|
173 |
HOLCF-WorkerWrapper |
|
174 |
HRB-Slicing |
|
175 |
HRB-Slicing-InformationFlowSlicing |
|
176 |
Jinja |
|
177 |
LatticeProperties |
|
178 |
LatticeProperties-MonoBoolTranAlgebra |
|
179 |
LatticeProperties-PseudoHoops |
|
180 |
Lower_Semicontinuous |
|
181 |
NormByEval |
|
182 |
Simpl |
|
183 |
Simpl-BDD |
|
184 |
Slicing |
|
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 |