wenzelm@10555: #!/usr/bin/env bash
wenzelm@2755: #
wenzelm@2755: # $Id$
wenzelm@9817: # Author: Markus Wenzel, TU Muenchen
wenzelm@2755: #
wenzelm@2902: # build - compile the Isabelle system and object-logics
wenzelm@2755: 
wenzelm@15844: if [ -L "$0" ]; then
wenzelm@15844:   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
wenzelm@15967:   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
wenzelm@15844: fi
wenzelm@15844: 
wenzelm@2755: 
wenzelm@4457: ## global settings
wenzelm@4457: 
wenzelm@15844: ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
wenzelm@4457: 
wenzelm@4457: 
wenzelm@2789: ## settings
wenzelm@2789: 
wenzelm@7889: export THIS_IS_ISABELLE_BUILD=true
wenzelm@15844: 
wenzelm@15967: PRG="$(basename "$0")"
wenzelm@15967: 
wenzelm@15967: ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
wenzelm@15967: source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
wenzelm@2755: 
wenzelm@2789: 
wenzelm@2879: ## diagnostics
wenzelm@2879: 
wenzelm@2879: function usage()
wenzelm@2879: {
wenzelm@2879:   echo
wenzelm@2879:   echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
wenzelm@2879:   echo
wenzelm@2879:   echo "  Options are:"
wenzelm@2879:   echo "    -a           all logics"
wenzelm@2902:   echo "    -b           batch mode"
wenzelm@6256:   echo "    -i           make images"
wenzelm@7889:   echo "    -m TARGET    make this target"
wenzelm@6256:   echo "    -t           make test"
wenzelm@2879:   echo
wenzelm@3184:   echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
wenzelm@2879:   echo "  in the distribution."
wenzelm@2879:   echo
wenzelm@2879:   exit 1
wenzelm@2879: }
wenzelm@2879: 
wenzelm@2879: function fail()
wenzelm@2879: {
wenzelm@2879:   echo "$1" >&2
wenzelm@2879:   exit 2
wenzelm@2879: }
wenzelm@2879: 
wenzelm@2879: 
wenzelm@2879: ## process command line
wenzelm@2879: 
wenzelm@2879: # options
wenzelm@2879: 
wenzelm@2879: ALL=""
wenzelm@2902: BATCH=""
wenzelm@7889: TARGETS=""
wenzelm@2755: 
wenzelm@15844: while getopts "abim:t" OPT
wenzelm@2879: do
wenzelm@2879:   case "$OPT" in
wenzelm@2879:     a)
wenzelm@2879:       ALL=true
wenzelm@2879:       ;;
wenzelm@2902:     b)
wenzelm@2902:       BATCH=true
wenzelm@2902:       ;;
wenzelm@6256:     i)
wenzelm@7889:       TARGETS="$TARGETS images"
wenzelm@7889:       ;;
wenzelm@7889:     m)
wenzelm@7889:       TARGETS="$TARGETS $OPTARG"
wenzelm@6256:       ;;
wenzelm@2918:     t)
wenzelm@7889:       TARGETS="$TARGETS test"
wenzelm@2918:       ;;
wenzelm@2879:     \?)
wenzelm@2879:       usage
wenzelm@2879:       ;;
wenzelm@2879:   esac
wenzelm@2879: done
wenzelm@2879: 
wenzelm@2879: shift $(($OPTIND - 1))
wenzelm@2879: 
wenzelm@2879: 
wenzelm@2879: # args
wenzelm@2879: 
wenzelm@2879: LOGICS="$@"
wenzelm@2879: 
wenzelm@4457: [ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
wenzelm@4457: [ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
wenzelm@4457: 
wenzelm@2879: 
wenzelm@2879: ## main
wenzelm@2879: 
wenzelm@2879: # tell the user about current values
wenzelm@2879: 
wenzelm@2902: if [ -z "$BATCH" ]; then
wenzelm@2902:   echo
wenzelm@2902:   echo "                *****************************"
wenzelm@2902:   echo "                * Welcome to Isabelle build *"
wenzelm@2902:   echo "                *****************************"
wenzelm@2902:   echo
wenzelm@2902:   echo "Please check $ISABELLE_HOME/etc/settings"
wenzelm@9789:   [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
wenzelm@5386:   echo "to make sure that Isabelle's ML system settings and compilation options"
wenzelm@5386:   echo "are appropriate."
wenzelm@2902:   echo
wenzelm@5386:   echo "The current values are:"
wenzelm@2902:   echo
wenzelm@2902:   echo "  ML_SYSTEM=$ML_SYSTEM"
wenzelm@2902:   echo "  ML_HOME=$ML_HOME"
wenzelm@2902:   echo "  ML_OPTIONS=$ML_OPTIONS"
wenzelm@7277:   echo "  ML_PLATFORM=$ML_PLATFORM"
wenzelm@5386:   echo
wenzelm@5386:   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
wenzelm@17576:   echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
wenzelm@2902: fi
wenzelm@2789: 
wenzelm@2789: 
wenzelm@2879: # check logics
wenzelm@2755: 
wenzelm@2902: if [ -z "$BATCH" ]; then
wenzelm@2902:   echo
wenzelm@2902:   echo
wenzelm@9817:   echo "Press RETURN to compilation of"
wenzelm@2902:   echo
wenzelm@2902: fi
wenzelm@2879: 
wenzelm@4457: 
wenzelm@4457: MAKE_LOGICS=""
wenzelm@2879: 
wenzelm@4457: for L in $LOGICS
wenzelm@4457: do
wenzelm@9789:   DIR="$ISABELLE_HOME/src/$L"
wenzelm@9789:   if [ -f "$DIR/IsaMakefile" ]; then
wenzelm@4457:     MAKE_LOGICS="$MAKE_LOGICS $L"
wenzelm@4457:   else
wenzelm@4457:     echo "No such logic: $L"
wenzelm@4457:   fi
wenzelm@4457: done
wenzelm@4457: 
wenzelm@2879: 
wenzelm@2902: if [ -z "$BATCH" ]; then
wenzelm@9789:   echo " $MAKE_LOGICS"
wenzelm@9817:   [ -n "$TARGETS" ] && echo "  (targets:$TARGETS)"
wenzelm@2902:   echo
wenzelm@2902:   read
wenzelm@2902: else
wenzelm@2902:   echo
wenzelm@9789:   echo "Isabelle build: $MAKE_LOGICS"
wenzelm@9817:   [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
wenzelm@2914:   echo
wenzelm@2902:   echo "ML_SYSTEM=$ML_SYSTEM"
wenzelm@2902:   echo "ML_HOME=$ML_HOME"
wenzelm@2902:   echo "ML_OPTIONS=$ML_OPTIONS"
wenzelm@7311:   echo "ML_PLATFORM=$ML_PLATFORM"
wenzelm@2902:   echo
wenzelm@5393:   echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
wenzelm@17649:   echo "HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
wenzelm@5393:   echo
wenzelm@2902: fi
wenzelm@2755: 
wenzelm@2755: 
wenzelm@2879: # build it
wenzelm@2879: 
wenzelm@10511: echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
wenzelm@18321: . "$ISABELLE_HOME/lib/scripts/timestart.bash"
wenzelm@2914: 
wenzelm@4457: for L in $MAKE_LOGICS
wenzelm@2755: do
kleing@14056:   ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
wenzelm@2755: done
wenzelm@2902: 
wenzelm@2914: echo -n "Finished at "; date
wenzelm@4457: 
wenzelm@18321: . "$ISABELLE_HOME/lib/scripts/timestop.bash"
wenzelm@18321: echo "$TIMES_REPORT"