build

* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.

* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution

#!/usr/bin/env bash
#
# $Id$
# 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

export THIS_IS_ISABELLE_BUILD=true

PRG="$(basename "$0")"

ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2


## 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"
  echo "  HOL_USEDIR_OPTIONS=$HOL_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 "HOL_USEDIR_OPTIONS=$HOL_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"; "$ISATOOL" make $TARGETS )
done

echo -n "Finished at "; date

. "$ISABELLE_HOME/lib/scripts/timestop.bash"
echo "$TIMES_REPORT"