#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: Standard statistics.
THIS="$(cd "$(dirname "$0")"; pwd)"
PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 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-Cardinals
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-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