Admin/isatest/isatest-stats
author haftmann
Thu, 18 Nov 2010 17:01:15 +0100
changeset 40602 91e583511113
parent 38561 d2a8087effc6
child 41646 167a045fade4
permissions -rwxr-xr-x
map_fun combinator in theory Fun

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

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

PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"

ISABELLE_SESSIONS="\
  HOL-Plain \
  HOL-Main \
  HOL \
  HOL-Proofs \
  HOL-Library \
  HOL-Algebra \
  HOL-Auth \
  HOL-Bali \
  HOL-Decision_Procs \
  HOL-Hoare \
  HOL-Hoare_Parallel \
  HOL-Imperative_HOL \
  HOL-Metis_Examples \
  HOL-MicroJava \
  HOL-Multivariate_Analysis \
  HOL-NSA \
  HOL-Nominal-Examples \
  HOL-Number_Theory \
  HOL-Old_Number_Theory \
  HOL-Predicate_Compile_Examples \
  HOL-Proofs-Extraction \
  HOL-Proofs-Lambda \
  HOL-SET_Protocol \
  HOL-UNITY \
  HOL-Word \
  HOL-Word-SMT_Examples \
  HOL-ex \
  HOLCF \
  IOA \
  ZF \
  ZF-Constructible \
  ZF-UNITY"

AFP_SESSIONS="\
  Coinductive \
  CoreC++ \
  Group-Ring-Module \
  Group-Ring-Module-Valuation \
  HOL-BytecodeLogicJmlTypes \
  HOL-Collections \
  HOL-DiskPaxos \
  HOL-FeatherweightJava \
  HOL-Fermat3_4 \
  HOL-Flyspeck-Tame \
  HOL-Free-Groups \
  HOL-GraphMarkingIBP \
  HOL-JiveDataStoreModel \
  HOL-Locally-Nameless-Sigma \
  HOL-Ordinals_and_Cardinals \
  HOL-POPLmark-deBruijn \
  HOL-Presburger-Automata \
  HOL-Program-Conflict-Analysis \
  HOL-RSAPSS \
  HOL-Recursion-Theory-I \
  HOL-SATSolverVerification \
  HOL-SIFPL \
  HOL-SenSocialChoice \
  HOL-SumSquares \
  HOL-Topology \
  HOL-Tree-Automata \
  HOL-Word-JinjaThreads \
  HOLCF-WorkerWrapper \
  HRB-Slicing \
  Jinja \
  Jinja-Slicing \
  LinearQuantifierElim \
  Simpl \
  Simpl-BDD \
  Slicing \
  Slicing-InformationFlowSlicing"

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