Admin/isatest/isatest-stats
author wenzelm
Thu, 25 Jun 2009 13:40:03 +0200
changeset 31802 a36b5e02c1ab
parent 31620 b0f6168d2b25
child 32276 756afe4a909a
permissions -rwxr-xr-x
more stats;

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: Standard statistics.

THIS=$(cd "$(dirname "$0")"; pwd -P)

PLATFORMS="at-poly at64-poly mac-poly-M4 mac-poly-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"

ISABELLE_SESSIONS="\
  HOL-Plain \
  HOL-Main \
  HOL \
  HOL-Algebra \
  HOL-Auth \
  HOL-Bali \
  HOL-Decision_Procs \
  HOL-Extraction \
  HOL-Hoare \
  HOL-HoareParallel \
  HOL-Lambda \
  HOL-Library \
  HOL-MetisExamples \
  HOL-MicroJava \
  HOL-NSA \
  HOL-NewNumberTheory \
  HOL-Nominal-Examples \
  HOL-NumberTheory \
  HOL-SET-Protocol \
  HOL-UNITY \
  HOL-Word \
  HOL-ex \
  HOLCF \
  IOA \
  ZF \
  ZF-Constructible \
  ZF-UNITY"

AFP_SESSIONS="\
  CoreC++ \
  HOL-BytecodeLogicJmlTypes \
  HOL-DiskPaxos \
  HOL-Fermat3_4 \
  HOL-Flyspeck-Tame \
  HOL-Group-Ring-Module \
  HOL-Jinja \
  HOL-JinjaThreads \
  HOL-JiveDataStoreModel \
  HOL-POPLmark-deBruijn \
  HOL-Program-Conflict-Analysis \
  HOL-RSAPSS \
  HOL-Recursion-Theory-I \
  HOL-SATSolverVerification \
  HOL-SIFPL \
  HOL-SenSocialChoice \
  HOL-Slicing \
  HOL-SumSquares \
  HOL-Topology \
  HOL-Valuation \
  LinearQuantifierElim \
  Simpl \
  Simpl-BDD"

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