--- a/Admin/isatest/isatest-statistics Thu Oct 04 14:42:47 2007 +0200
+++ b/Admin/isatest/isatest-statistics Thu Oct 04 16:21:31 2007 +0200
@@ -5,21 +5,20 @@
#
# DESCRIPTION: Produce statistics from isatest session logs.
-ISATEST_LOG=~isatest/log
-
## platform settings
case $(uname) in
- SunOS)
- ZGREP=xgrep
- TE="png color"
- ;;
- *)
- ZGREP=zgrep
- TE="png"
- ;;
+ SunOS)
+ ZGREP=xgrep
+ TE="png color"
+ ;;
+ *)
+ ZGREP=zgrep
+ TE="png"
+ ;;
esac
+
## diagnostics
PRG="$(basename "$0")"
@@ -52,6 +51,14 @@
TIMESPAN="$1"; shift
SESSIONS="$@"
+if [ "$PLATFORM" = afp ]; then
+ LOG_DIR=~isatest/afp-log
+ LOG_NAME="afp-test-devel*"
+else
+ LOG_DIR=~isatest/log
+ LOG_NAME="isatest-makeall-${PLATFORM}*"
+fi
+
## main
@@ -60,10 +67,10 @@
mkdir -p "$DIR" || fail "Bad directory: $DIR"
$ZGREP "^Finished .*elapsed" \
- $(find "$ISATEST_LOG" -name "isatest-makeall-${PLATFORM}*" -ctime "-${TIMESPAN}") | \
+ $(find "$LOG_DIR" -name "$LOG_NAME" -ctime "-${TIMESPAN}") | \
perl -e '
while (<>) {
- if (m/isatest-makeall-.*-(\d+)-(\d+)-(\d+)-.*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
+ if (m/(\d\d\d\d)-(\d\d)-(\d\d).*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
my $year = $1;
my $month = $2;
my $day = $3;
--- a/Admin/isatest/isatest-stats Thu Oct 04 14:42:47 2007 +0200
+++ b/Admin/isatest/isatest-stats Thu Oct 04 16:21:31 2007 +0200
@@ -7,8 +7,9 @@
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e at-poly-5.1-para-e at64-poly-5.1-para-e at-mac-poly-5.1-para-e"
-SESSIONS="\
+PLATFORMS="at-poly at-sml-dev at64-poly-e at64-poly-5.1-para-e at-mac-poly-5.1-para-e afp"
+
+ISABELLE_SESSIONS="\
HOL \
HOL-Algebra \
HOL-Auth \
@@ -30,8 +31,27 @@
ZF-Constructible\
ZF-UNITY"
+AFP_SESSIONS="\
+ CoreC++\
+ HOL-DiskPaxos\
+ HOL-Fermat3_4\
+ HOL-Flyspeck-Tame\
+ HOL-Group-Ring-Module\
+ HOL-Jinja\
+ HOL-JiveDataStoreModel\
+ HOL-POPLmark-deBruijn\
+ HOL-RSAPSS\
+ HOL-SumSquares\
+ HOL-Valuation"
+
for PLATFORM in $PLATFORMS
do
+ if [ "$PLATFORM" = afp ]; then
+ SESSIONS="$AFP_SESSIONS"
+ else
+ SESSIONS="$ISABELLE_SESSIONS"
+ fi
+
"$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
cat > "stats/$PLATFORM.html" <<EOF
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">