equal
deleted
inserted
replaced
|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # Author: Makarius |
|
5 # |
|
6 # DESCRIPTION: Standard statistics. |
|
7 |
|
8 THIS=$(cd "$(dirname "$0")"; pwd -P) |
|
9 |
|
10 PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e" |
|
11 SESSIONS="\ |
|
12 HOL \ |
|
13 HOL-Algebra \ |
|
14 HOL-Auth \ |
|
15 HOL-Bali \ |
|
16 HOL-Complex \ |
|
17 HOL-Complex-ex \ |
|
18 HOL-Extraction \ |
|
19 HOL-Hoare \ |
|
20 HOL-HoareParallel \ |
|
21 HOL-Lambda \ |
|
22 HOL-MicroJava \ |
|
23 HOL-NumberTheory \ |
|
24 HOL-SET-Protocol \ |
|
25 HOL-UNITY \ |
|
26 HOL-ex \ |
|
27 ZF \ |
|
28 ZF-Constructible\ |
|
29 ZF-UNITY" |
|
30 |
|
31 for PLATFORM in $PLATFORMS |
|
32 do |
|
33 "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS |
|
34 cat > "stats/$PLATFORM.html" <<EOF |
|
35 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN"> |
|
36 <html> |
|
37 <head><title>Development Snapshot -- Performance Statistics</title></head> |
|
38 |
|
39 <body> |
|
40 <h1>$PLATFORM</h1> |
|
41 EOF |
|
42 |
|
43 for SESSION in $SESSIONS |
|
44 do |
|
45 echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html" |
|
46 done |
|
47 |
|
48 echo "</body>" >> "stats/$PLATFORM.html" |
|
49 echo "</html>" >> "stats/$PLATFORM.html" |
|
50 |
|
51 done |