Rewrite the Probability theory.
Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: Standard statistics.
THIS=$(cd "$(dirname "$0")"; pwd -P)
PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly mac-poly-M4 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-Plain \
HOL-Main \
HOL \
HOL-Proofs \
HOL-Library \
HOL-Algebra \
HOL-Auth \
HOL-Bali \
HOL-Decision_Procs \
HOL-Hoare \
HOL-Hoare_Parallel \
HOL-Imperative_HOL \
HOL-Metis_Examples \
HOL-MicroJava \
HOL-Multivariate_Analysis \
HOL-NSA \
HOL-Nominal-Examples \
HOL-Number_Theory \
HOL-Old_Number_Theory \
HOL-Predicate_Compile_Examples \
HOL-Proofs-Extraction \
HOL-Proofs-Lambda \
HOL-SET_Protocol \
HOL-UNITY \
HOL-Word \
HOL-Word-SMT_Examples \
HOL-ex \
HOLCF \
IOA \
ZF \
ZF-Constructible \
ZF-UNITY"
AFP_SESSIONS="\
Coinductive \
CoreC++ \
Group-Ring-Module \
Group-Ring-Module-Valuation \
HOL-BytecodeLogicJmlTypes \
HOL-Collections \
HOL-DiskPaxos \
HOL-FeatherweightJava \
HOL-Fermat3_4 \
HOL-Flyspeck-Tame \
HOL-Free-Groups \
HOL-GraphMarkingIBP \
HOL-JiveDataStoreModel \
HOL-Locally-Nameless-Sigma \
HOL-Ordinals_and_Cardinals \
HOL-POPLmark-deBruijn \
HOL-Presburger-Automata \
HOL-Program-Conflict-Analysis \
HOL-RSAPSS \
HOL-Recursion-Theory-I \
HOL-SATSolverVerification \
HOL-SIFPL \
HOL-SenSocialChoice \
HOL-SumSquares \
HOL-Topology \
HOL-Tree-Automata \
HOL-Word-JinjaThreads \
HOLCF-WorkerWrapper \
HRB-Slicing \
Jinja \
Jinja-Slicing \
LinearQuantifierElim \
Simpl \
Simpl-BDD \
Slicing \
Slicing-InformationFlowSlicing"
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