more complete stats, including small sessions which provide some clues on main HOL baseline performance;
#!/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-Auth \
HOL-Bali \
HOL-Boogie-Examples \
HOL-Decision_Procs \
HOL-Hahn_Banach \
HOL-Hoare \
HOL-Hoare_Parallel \
HOL-IMPP \
HOL-IOA \
HOL-Imperative_HOL \
HOL-Import \
HOL-Induct \
HOL-Isar_Examples \
HOL-Lattice \
HOL-Library-Codegenerator_Test \
HOL-Matrix \
HOL-Metis_Examples \
HOL-MicroJava \
HOL-Mirabelle \
HOL-Mutabelle \
HOL-NanoJava \
HOL-Nitpick_Examples \
HOL-Nominal-Examples
HOL-Number_Theory \
HOL-Old_Number_Theory \
HOL-Predicate_Compile_Examples \
HOL-Probability
HOL-Prolog \
HOL-Proofs-Extraction \
HOL-Proofs-Lambda \
HOL-Proofs-ex \
HOL-Quotient_Examples \
HOL-SET_Protocol \
HOL-SPARK-Examples \
HOL-SPARK-Manual \
HOL-Statespace \
HOL-TPTP \
HOL-UNITY \
HOL-Unix \
HOL-Word-Examples \
HOL-Word-SMT_Examples \
HOL-ZF
HOL-ex \
HOLCF-FOCUS \
HOLCF-IMP \
HOLCF-Library \
HOLCF-Tutorial \
HOLCF-ex \
IOA-ABP \
IOA-NTP \
IOA-Storage \
IOA-ex \
TLA-Buffer \
TLA-Inc \
TLA-Memory"
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 \
HOLCF \
HOLCF-Shivers-CFA \
HOLCF-Stream-Fusion \
HOLCF-WorkerWrapper \
HRB-Slicing \
HRB-Slicing-InformationFlowSlicing \
Jinja \
Jinja \
LatticeProperties \
LatticeProperties-MonoBoolTranAlgebra \
LatticeProperties-PseudoHoops \
Lower_Semicontinuous \
NormByEval \
Simpl \
Simpl-BDD \
Slicing \
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