| author | wenzelm |
| Tue Sep 19 23:01:52 2006 +0200 (2006-09-19) | |
| changeset 20618 | 3f763be47c2f |
| parent 20617 | ca59894f70dc |
| child 20619 | 02e9b54b18fd |
| permissions | -rwxr-xr-x |
| wenzelm@20613 | 1 |
#!/usr/bin/env bash |
| wenzelm@20613 | 2 |
# |
| wenzelm@20613 | 3 |
# $Id$ |
| wenzelm@20613 | 4 |
# Author: Makarius |
| wenzelm@20613 | 5 |
# |
| wenzelm@20613 | 6 |
# DESCRIPTION: Standard statistics. |
| wenzelm@20613 | 7 |
|
| wenzelm@20613 | 8 |
THIS=$(cd "$(dirname "$0")"; pwd -P) |
| wenzelm@20613 | 9 |
|
| wenzelm@20618 | 10 |
PLATFORMS="at-poly at-sml-dev" |
| wenzelm@20618 | 11 |
SESSIONS="\ |
| wenzelm@20618 | 12 |
HOL \ |
| wenzelm@20618 | 13 |
HOL-Algebra \ |
| wenzelm@20618 | 14 |
HOL-Auth \ |
| wenzelm@20618 | 15 |
HOL-Bali \ |
| wenzelm@20618 | 16 |
HOL-Complex \ |
| wenzelm@20618 | 17 |
HOL-Extraction \ |
| wenzelm@20618 | 18 |
HOL-Hoare \ |
| wenzelm@20618 | 19 |
HOL-HoareParallel \ |
| wenzelm@20618 | 20 |
HOL-Lambda \ |
| wenzelm@20618 | 21 |
HOL-MicroJava \ |
| wenzelm@20618 | 22 |
HOL-NumberTheory \ |
| wenzelm@20618 | 23 |
HOL-SET-Protocol \ |
| wenzelm@20618 | 24 |
HOL-UNITY \ |
| wenzelm@20618 | 25 |
HOL-ex \ |
| wenzelm@20618 | 26 |
ZF \ |
| wenzelm@20618 | 27 |
ZF-Constructible" |
| wenzelm@20618 | 28 |
|
| wenzelm@20618 | 29 |
for PLATFORM in $PLATFORMS |
| wenzelm@20615 | 30 |
do |
| wenzelm@20618 | 31 |
"$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 100 $SESSIONS |
| wenzelm@20618 | 32 |
cat > "stats/$PLATFORM.html" <<EOF |
| wenzelm@20618 | 33 |
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN"> |
| wenzelm@20618 | 34 |
<html> |
| wenzelm@20618 | 35 |
<head><title> Development Snapshot -- Statistics</title></head> |
| wenzelm@20618 | 36 |
|
| wenzelm@20618 | 37 |
<body> |
| wenzelm@20618 | 38 |
<h1>$PLATFORM</h1> |
| wenzelm@20618 | 39 |
EOF |
| wenzelm@20618 | 40 |
|
| wenzelm@20618 | 41 |
for SESSION in $SESSIONS |
| wenzelm@20618 | 42 |
do |
| wenzelm@20618 | 43 |
echo "<br><img src="$PLATFORM/$SESSION.png">" >> "stats/$PLATFORM.html" |
| wenzelm@20615 | 44 |
done |
| wenzelm@20618 | 45 |
|
| wenzelm@20618 | 46 |
echo "</body>" >> "stats/$PLATFORM.html" |
| wenzelm@20618 | 47 |
echo "</html>" >> "stats/$PLATFORM.html" |
| wenzelm@20618 | 48 |
|
| wenzelm@20618 | 49 |
done |