|
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 |
|
|
20615
|
10 |
for PLATFORM in at-poly at-sml-dev
|
|
|
11 |
do
|
|
|
12 |
"$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 1000 \
|
|
|
13 |
HOL \
|
|
|
14 |
HOL-Algebra \
|
|
|
15 |
HOL-Auth \
|
|
|
16 |
HOL-Bali \
|
|
|
17 |
HOL-Complex \
|
|
|
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 |
done
|