#!/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
