Admin/isatest/isatest-stats
author wenzelm
Fri, 17 Aug 2012 11:37:14 +0200
changeset 48836 90a0af19004c
parent 47044 1ab41ea5b1c6
child 49310 6e30078de4f0
permissions -rwxr-xr-x
tuned;

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

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

PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 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
  HOL-Main
  HOL-Plain
  HOL-Base
  HOL-Library
  HOL-Algebra
  HOL-Auth
  HOL-Bali
  HOL-Boogie
  HOL-Boogie-Examples
  HOL-Decision_Procs
  HOL-Hahn_Banach
  HOL-Hoare
  HOL-Hoare_Parallel
  HOL-IMP
  HOL-IMPP
  HOL-IOA
  HOL-Imperative_HOL
  HOL-Import
  HOL-Induct
  HOL-Isar_Examples
  HOL-Lattice
  HOL-Library-Codegenerator_Test
  HOL-Matrix_LP
  HOL-Metis_Examples
  HOL-MicroJava
  HOL-Mirabelle
  HOL-Multivariate_Analysis
  HOL-Mutabelle
  HOL-NSA
  HOL-NanoJava
  HOL-Nitpick_Examples
  HOL-Nominal
  HOL-Nominal-Examples
  HOL-Number_Theory
  HOL-Old_Number_Theory
  HOL-Predicate_Compile_Examples
  HOL-Probability
  HOL-Prolog
  HOL-Proofs
  HOL-Proofs-Extraction
  HOL-Proofs-Lambda
  HOL-Proofs-ex
  HOL-Quickcheck_Examples
  HOL-Quotient_Examples
  HOL-SET_Protocol
  HOL-SPARK
  HOL-SPARK-Examples
  HOL-SPARK-Manual
  HOL-Statespace
  HOL-TPTP
  HOL-UNITY
  HOL-Unix
  HOL-Word
  HOL-Word-Examples
  HOL-Word-SMT_Examples
  HOL-ZF
  HOL-ex
  HOL4
  HOLCF
  HOLCF-FOCUS
  HOLCF-IMP
  HOLCF-Library
  HOLCF-Tutorial
  HOLCF-ex
  IOA
  IOA-ABP
  IOA-NTP
  IOA-Storage
  IOA-ex
  TLA
  TLA-Buffer
  TLA-Inc
  TLA-Memory
  HOL-Datatype_Benchmark
  HOL-Record_Benchmark"

AFP_SESSIONS="
  ArrowImpossibilityGS
  Coinductive
  CoreC++
  HOL-AVL-Trees
  HOL-Abstract-Hoare-Logics
  HOL-Abstract-Rewriting
  HOL-BinarySearchTree
  HOL-Binomial-Heaps
  HOL-Binomial-Queues
  HOL-BytecodeLogicJmlTypes
  HOL-Category
  HOL-Category2
  HOL-Cauchy
  HOL-ClockSynchInst
  HOL-CofGroups
  HOL-Collections
  HOL-Compiling-Exceptions-Correctly
  HOL-Completeness
  HOL-DPT-SAT-Solver
  HOL-DataRefinementIBP
  HOL-Depth-First-Search
  HOL-DiskPaxos
  HOL-Example-Submission
  HOL-FFT
  HOL-FOL-Fitting
  HOL-FeatherweightJava
  HOL-FileRefinement
  HOL-FinFun
  HOL-Finger-Trees
  HOL-Flyspeck-Tame
  HOL-Free-Boolean-Algebra
  HOL-Free-Groups
  HOL-FunWithFunctions
  HOL-FunWithTilings
  HOL-Functional-Automata
  HOL-Gauss-Jordan-Elim-Fun
  HOL-GenClock
  HOL-General-Triangle
  HOL-GraphMarkingIBP
  HOL-HotelKeyCards
  HOL-Huffman
  HOL-Integration
  HOL-JiveDataStoreModel
  HOL-KBPs
  HOL-Lazy-Lists-II
  HOL-LightweightJava
  HOL-List-Index
  HOL-Locally-Nameless-Sigma
  HOL-Marriage
  HOL-Matrix
  HOL-Max-Card-Matching
  HOL-MiniML
  HOL-MuchAdoAboutTwo
  HOL-Multivariate_Analysis
  HOL-Myhill-Nerode
  HOL-Nominal
  HOL-Nominal-Lam-ml-Normalization
  HOL-Nominal-SequentInvertibility
  HOL-Ordinal
  HOL-Ordinals_and_Cardinals
  HOL-POPLmark-deBruijn
  HOL-Perfect-Number-Thm
  HOL-Polynomials
  HOL-Presburger-Automata
  HOL-Program-Conflict-Analysis
  HOL-Ramsey-Infinite
  HOL-Recursion-Theory-I
  HOL-Regular-Sets
  HOL-Robbins-Conjecture
  HOL-SATSolverVerification
  HOL-SIFPL
  HOL-SenSocialChoice
  HOL-Statecharts
  HOL-Topology
  HOL-Transitive-Closure
  HOL-Tree-Automata
  HOL-Verified-Prover
  HOL-Word
  HOL-Word-RIPEMD-160-SPARK
  HOL-Word-JinjaThreads-Basic-JinjaThreads
  HOLCF
  HOLCF-Shivers-CFA
  HOLCF-Stream-Fusion
  HOLCF-WorkerWrapper
  HRB-Slicing
  HRB-Slicing-InformationFlowSlicing
  Jinja
  LatticeProperties
  LatticeProperties-MonoBoolTranAlgebra
  LatticeProperties-PseudoHoops
  Lower_Semicontinuous
  NormByEval
  Simpl
  Simpl-BDD
  Slicing
  Slicing-InformationFlowSlicing
  VolpanoSmith"


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