build

added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization

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