wenzelm@3007: #!/bin/bash
wenzelm@2755: #
wenzelm@2755: # $Id$
wenzelm@2755: #
wenzelm@2902: # build - compile the Isabelle system and object-logics
wenzelm@2755: 
wenzelm@2755: 
wenzelm@2789: ## settings
wenzelm@2789: 
wenzelm@2789: PRG=$(basename $0)
wenzelm@2755: 
wenzelm@2789: ISABELLE_HOME=$(dirname $0)
wenzelm@2789: . $ISABELLE_HOME/lib/scripts/getsettings || \
wenzelm@2936:   { echo "$PRG probably not called from its original place!"; 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@2918:   echo "    -t           run tests"
wenzelm@2879:   echo
wenzelm@2879:   echo "  Compile the named LOGICS (default $DEFAULT_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@2918: TEST=""
wenzelm@2755: 
wenzelm@2918: while getopts "abt" 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@2918:     t)
wenzelm@2918:       TEST=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@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@2902:   [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
wenzelm@2902:   echo "to make sure that Isabelle's ML system settings are appropriate."
wenzelm@2902:   echo
wenzelm@2902:   echo "Your 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@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@2902:   echo "Press RETURN to start compilation (including parents) of:"
wenzelm@2902:   echo
wenzelm@2902: fi
wenzelm@2879: 
wenzelm@2879: [ -z "$LOGICS" ] && LOGICS=$DEFAULT_LOGIC
wenzelm@2879: 
wenzelm@2879: if [ -n "$ALL" ]; then
wenzelm@2879:   LOGICS=""
wenzelm@2879:   for DIR in $ISABELLE_HOME/src/*
wenzelm@2879:   do
wenzelm@2879:     if [ -f $DIR/IsaMakefile ]; then
wenzelm@2879:       L=$(basename $DIR)
wenzelm@2879:       LOGICS="$LOGICS $L"
wenzelm@2879:     fi
wenzelm@2879:   done
wenzelm@2879: else
wenzelm@2879:   for L in $LOGICS
wenzelm@2879:   do
wenzelm@2879:     DIR=$ISABELLE_HOME/src/$L
wenzelm@2879:     [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
wenzelm@2879:   done
wenzelm@2879: fi
wenzelm@2879: 
wenzelm@2902: if [ -z "$BATCH" ]; then
wenzelm@2902:   echo " " $LOGICS
wenzelm@2902:   echo
wenzelm@2902:   read
wenzelm@2902: else
wenzelm@2902:   echo
wenzelm@2914:   echo "Isabelle build:" $LOGICS
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@2902:   echo
wenzelm@2902: fi
wenzelm@2755: 
wenzelm@2755: 
wenzelm@2879: # build it
wenzelm@2879: 
wenzelm@2914: echo
wenzelm@2914: echo -n "Started at "; date
wenzelm@2914: echo
wenzelm@2914: 
wenzelm@2781: export THIS_IS_ISABELLE_BUILD=true
wenzelm@2755: 
wenzelm@2879: for L in $LOGICS
wenzelm@2755: do
wenzelm@2918:   ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TEST )
wenzelm@2755: done
wenzelm@2902: 
wenzelm@2914: echo
wenzelm@2914: echo -n "Finished at "; date
wenzelm@2914: echo