#!/usr/bin/env bash
#
# $Id$
# Author: Makarius
#
# DESCRIPTION: Standard statistics.
THIS=$(cd "$(dirname "$0")"; pwd -P)
PLATFORMS="at-poly at-sml-dev at64-poly at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp"
ISABELLE_SESSIONS="\
HOL-Plain \
HOL \
HOL-Algebra \
HOL-Auth \
HOL-Bali \
HOL-Complex \
HOL-Complex-ex \
HOL-Extraction \
HOL-Hoare \
HOL-HoareParallel \
HOL-Lambda \
HOL-Library \
HOL-MetisExamples \
HOL-MicroJava \
HOL-NSA \
HOL-Nominal-Examples \
HOL-NumberTheory \
HOL-SET-Protocol \
HOL-UNITY \
HOL-Word \
HOL-ex \
ZF \
ZF-Constructible\
ZF-UNITY"
AFP_SESSIONS="\
CoreC++\
LinearQuantifierElim\
HOL-DiskPaxos\
HOL-Fermat3_4\
HOL-Flyspeck-Tame\
HOL-Group-Ring-Module\
HOL-JinjaThreads\
HOL-Jinja\
HOL-JiveDataStoreModel\
HOL-POPLmark-deBruijn\
HOL-Program-Conflict-Analysis\
HOL-RSAPSS\
HOL-Recursion-Theory-I\
HOL-SumSquares\
HOL-Topology\
HOL-Valuation\
Simpl-BDD\
Simpl"
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">
<html>
<head><title>Development Snapshot -- Performance Statistics</title></head>
<body>
<h1>$PLATFORM</h1>
EOF
for SESSION in $SESSIONS
do
echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
done
echo "</body>" >> "stats/$PLATFORM.html"
echo "</html>" >> "stats/$PLATFORM.html"
done