build

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: Markus Wenzel, TU Muenchen
+
−#
+
−# build - compile the Isabelle system and object-logics
+
−
+
−if [ -L "$0" ]; then
+
−  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+
−  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+
−fi
+
−
+
−
+
−## global settings
+
−
+
−ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
+
−
+
−
+
−## settings
+
−
+
−PRG="$(basename "$0")"
+
−
+
−ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
+
−source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+
−
+
−ISABELLE_OUTPUT="$ISABELLE_HOME/heaps/$ML_IDENTIFIER"
+
−ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
+
−
+
−
+
−## diagnostics
+
−
+
−function usage()
+
−{
+
−  echo
+
−  echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
+
−  echo
+
−  echo "  Options are:"
+
−  echo "    -a           all logics"
+
−  echo "    -b           batch mode"
+
−  echo "    -i           make images"
+
−  echo "    -m TARGET    make this target"
+
−  echo "    -t           make test"
+
−  echo
+
−  echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
+
−  echo "  in the distribution."
+
−  echo
+
−  exit 1
+
−}
+
−
+
−function fail()
+
−{
+
−  echo "$1" >&2
+
−  exit 2
+
−}
+
−
+
−
+
−## process command line
+
−
+
−# options
+
−
+
−ALL=""
+
−BATCH=""
+
−TARGETS=""
+
−
+
−while getopts "abim:t" OPT
+
−do
+
−  case "$OPT" in
+
−    a)
+
−      ALL=true
+
−      ;;
+
−    b)
+
−      BATCH=true
+
−      ;;
+
−    i)
+
−      TARGETS="$TARGETS images"
+
−      ;;
+
−    m)
+
−      TARGETS="$TARGETS $OPTARG"
+
−      ;;
+
−    t)
+
−      TARGETS="$TARGETS test"
+
−      ;;
+
−    \?)
+
−      usage
+
−      ;;
+
−  esac
+
−done
+
−
+
−shift $(($OPTIND - 1))
+
−
+
−
+
−# args
+
−
+
−LOGICS="$@"
+
−
+
−[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
+
−[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
+
−
+
−
+
−## main
+
−
+
−# tell the user about current values
+
−
+
−if [ -z "$BATCH" ]; then
+
−  echo
+
−  echo "                *****************************"
+
−  echo "                * Welcome to Isabelle build *"
+
−  echo "                *****************************"
+
−  echo
+
−  echo "Please check $ISABELLE_HOME/etc/settings"
+
−  [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
+
−  echo "to make sure that Isabelle's ML system settings and compilation options"
+
−  echo "are appropriate."
+
−  echo
+
−  echo "The current values are:"
+
−  echo
+
−  echo "  ML_SYSTEM=$ML_SYSTEM"
+
−  echo "  ML_HOME=$ML_HOME"
+
−  echo "  ML_OPTIONS=$ML_OPTIONS"
+
−  echo "  ML_PLATFORM=$ML_PLATFORM"
+
−  echo
+
−  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
+
−fi
+
−
+
−
+
−# check logics
+
−
+
−if [ -z "$BATCH" ]; then
+
−  echo
+
−  echo
+
−  echo "Press RETURN to compilation of"
+
−  echo
+
−fi
+
−
+
−
+
−MAKE_LOGICS=""
+
−
+
−for L in $LOGICS
+
−do
+
−  DIR="$ISABELLE_HOME/src/$L"
+
−  if [ -f "$DIR/IsaMakefile" ]; then
+
−    MAKE_LOGICS="$MAKE_LOGICS $L"
+
−  else
+
−    echo "No such logic: $L"
+
−  fi
+
−done
+
−
+
−
+
−if [ -z "$BATCH" ]; then
+
−  echo " $MAKE_LOGICS"
+
−  [ -n "$TARGETS" ] && echo "  (targets:$TARGETS)"
+
−  echo
+
−  read
+
−else
+
−  echo
+
−  echo "Isabelle build: $MAKE_LOGICS"
+
−  [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
+
−  echo
+
−  echo "ML_SYSTEM=$ML_SYSTEM"
+
−  echo "ML_HOME=$ML_HOME"
+
−  echo "ML_OPTIONS=$ML_OPTIONS"
+
−  echo "ML_PLATFORM=$ML_PLATFORM"
+
−  echo
+
−  echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
+
−  echo
+
−fi
+
−
+
−
+
−# build it
+
−
+
−echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
+
−. "$ISABELLE_HOME/lib/scripts/timestart.bash"
+
−
+
−for L in $MAKE_LOGICS
+
−do
+
−  ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make $TARGETS )
+
−done
+
−
+
−echo -n "Finished at "; date
+
−
+
−. "$ISABELLE_HOME/lib/scripts/timestop.bash"
+
−echo "$TIMES_REPORT"