|
20613
|
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 |
|
|
20618
|
10 |
PLATFORMS="at-poly at-sml-dev"
|
|
|
11 |
SESSIONS="\
|
|
|
12 |
HOL \
|
|
|
13 |
HOL-Algebra \
|
|
|
14 |
HOL-Auth \
|
|
|
15 |
HOL-Bali \
|
|
|
16 |
HOL-Complex \
|
|
|
17 |
HOL-Extraction \
|
|
|
18 |
HOL-Hoare \
|
|
|
19 |
HOL-HoareParallel \
|
|
|
20 |
HOL-Lambda \
|
|
|
21 |
HOL-MicroJava \
|
|
|
22 |
HOL-NumberTheory \
|
|
|
23 |
HOL-SET-Protocol \
|
|
|
24 |
HOL-UNITY \
|
|
|
25 |
HOL-ex \
|
|
|
26 |
ZF \
|
|
|
27 |
ZF-Constructible"
|
|
|
28 |
|
|
|
29 |
for PLATFORM in $PLATFORMS
|
|
20615
|
30 |
do
|
|
20618
|
31 |
"$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 100 $SESSIONS
|
|
|
32 |
cat > "stats/$PLATFORM.html" <<EOF
|
|
|
33 |
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
|
|
|
34 |
<html>
|
|
|
35 |
<head><title> Development Snapshot -- Statistics</title></head>
|
|
|
36 |
|
|
|
37 |
<body>
|
|
|
38 |
<h1>$PLATFORM</h1>
|
|
|
39 |
EOF
|
|
|
40 |
|
|
|
41 |
for SESSION in $SESSIONS
|
|
|
42 |
do
|
|
|
43 |
echo "<br><img src="$PLATFORM/$SESSION.png">" >> "stats/$PLATFORM.html"
|
|
20615
|
44 |
done
|
|
20618
|
45 |
|
|
|
46 |
echo "</body>" >> "stats/$PLATFORM.html"
|
|
|
47 |
echo "</html>" >> "stats/$PLATFORM.html"
|
|
|
48 |
|
|
|
49 |
done
|