#!/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-poly-M8-skip_proofs mac-poly64-M8 at-sml-dev"
ISABELLE_SESSIONS="
HOL
HOL-Algebra
HOL-Auth
HOL-BNF
HOL-BNF-Examples
HOL-BNF-LFP
HOL-BNF-Nitpick_Examples
HOL-Bali
HOL-Cardinals
HOL-Cardinals-Base
HOL-Codegenerator_Test
HOL-Datatype_Benchmark
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
HOL-Matrix_LP
HOL-Metis_Examples
HOL-MicroJava
HOL-Mirabelle
HOL-Mirabelle-ex
HOL-Multivariate_Analysis
HOL-Mutabelle
HOL-NSA
HOL-NSA-Examples
HOL-NanoJava
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_Benchmark
HOL-Quickcheck_Examples
HOL-Quotient_Examples
HOL-Record_Benchmark
HOL-SET_Protocol
HOL-SPARK
HOL-SPARK-Examples
HOL-SPARK-Manual
HOL-Statespace
HOL-TLA
HOL-TLA-Buffer
HOL-TLA-Inc
HOL-TLA-Memory
HOL-TPTP
HOL-UNITY
HOL-Unix
HOL-Word
HOL-Word-Examples
HOL-Word-SMT_Examples
HOL-ZF
HOL-ex
HOLCF
HOLCF-FOCUS
HOLCF-IMP
HOLCF-Library
HOLCF-Tutorial
HOLCF-ex
IOA
IOA-ABP
IOA-NTP
IOA-Storage
IOA-ex
Pure
Spec_Check
ZF
ZF-AC
ZF-Coind
ZF-Constructible
ZF-IMP
ZF-Induct
ZF-Resid
ZF-UNITY
ZF-ex
"
AFP_SESSIONS="
AVL-Trees
Abortable_Linearizable_Modules
Abstract-Hoare-Logics
Abstract-Rewriting
ArrowImpossibilityGS
AutoFocus-Stream
BDD
BinarySearchTree
Binomial-Heaps
Binomial-Queues
Bondy
BytecodeLogicJmlTypes
CCS
Category
Category2
Cauchy
Circus
ClockSynchInst
CofGroups
Coinductive
Collections
Compiling-Exceptions-Correctly
Completeness
Containers
CoreC++
DPT-SAT-Solver
DataRefinementIBP
Datatype_Order_Generator
Depth-First-Search
Dijkstra_Shortest_Path
DiskPaxos
Efficient-Mergesort
Example-Submission
FFT
FOL-Fitting
FeatherweightJava
Fermat3_4
FileRefinement
FinFun
Finger-Trees
Flyspeck-Tame
Free-Boolean-Algebra
Free-Groups
FunWithFunctions
FunWithTilings
Functional-Automata
Gauss-Jordan-Elim-Fun
GenClock
General-Triangle
Girth_Chromatic
GraphMarkingIBP
Graph_Theory
Group-Ring-Module
HRB-Slicing
Heard_Of
HotelKeyCards
Huffman
Impossible_Geometry
Inductive_Confidentiality
InformationFlowSlicing
Integration
Jinja
JinjaThreads
JiveDataStoreModel
KBPs
Kleene_Algebra
Lam-ml-Normalization
LatticeProperties
Launchbury
Lazy-Lists-II
LightweightJava
LinearQuantifierElim
List-Index
List-Infinite
Locally-Nameless-Sigma
Lower_Semicontinuous
Markov_Models
Marriage
Matrix
Max-Card-Matching
MiniML
MonoBoolTranAlgebra
MuchAdoAboutTwo
Myhill-Nerode
Nat-Interval-Logic
Nominal2
NormByEval
Open_Induction
Ordinal
Ordinals_and_Cardinals
Ordinary_Differential_Equations
PCF
POPLmark-deBruijn
Perfect-Number-Thm
Pi_Calculus
Polynomials
Possibilistic_Noninterference
Presburger-Automata
Program-Conflict-Analysis
PseudoHoops
Psi_Calculi
RIPEMD-160-SPARK
RSAPSS
Ramsey-Infinite
Rank_Nullity_Theorem
Recursion-Theory-I
Refine_Monadic
Regular-Sets
Ribbon_Proofs
Robbins-Conjecture
SATSolverVerification
SIFPL
SenSocialChoice
Separation_Algebra
Separation_Logic_Imperative_HOL
SequentInvertibility
Shivers-CFA
ShortestPath
Simpl
Slicing
Sqrt_Babylonian
Statecharts
Stream-Fusion
Stuttering_Equivalence
SumSquares
TLA
Tarskis_Geometry
Topology
Transitive-Closure
Transitive-Closure-II
Tree-Automata
Tycon
Valuation
Verified-Prover
VolpanoSmith
Well_Quasi_Orders
WorkerWrapper
"
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