build
author wenzelm
Thu Aug 19 12:43:02 1999 +0200 (1999-08-19)
changeset 7277 bb9502f9154a
parent 6256 e17fb80b3ce1
child 7311 1ef2c659023d
permissions -rwxr-xr-x
improved messages;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # build - compile the Isabelle system and object-logics
     6 
     7 
     8 ## global settings
     9 
    10 ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
    11 
    12 
    13 ## settings
    14 
    15 PRG=$(basename $0)
    16 
    17 ISABELLE_HOME=$(dirname $0)
    18 . $ISABELLE_HOME/lib/scripts/getsettings || \
    19   { echo "$PRG probably not called from its original place!"; exit 2; }
    20 
    21 
    22 ## diagnostics
    23 
    24 function usage()
    25 {
    26   echo
    27   echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
    28   echo
    29   echo "  Options are:"
    30   echo "    -a           all logics"
    31   echo "    -b           batch mode"
    32   echo "    -i           make images"
    33   echo "    -t           make test"
    34   echo
    35   echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
    36   echo "  in the distribution."
    37   echo
    38   exit 1
    39 }
    40 
    41 function fail()
    42 {
    43   echo "$1" >&2
    44   exit 2
    45 }
    46 
    47 
    48 ## process command line
    49 
    50 # options
    51 
    52 ALL=""
    53 BATCH=""
    54 IMAGES=""
    55 TEST=""
    56 
    57 while getopts "abit" OPT
    58 do
    59   case "$OPT" in
    60     a)
    61       ALL=true
    62       ;;
    63     b)
    64       BATCH=true
    65       ;;
    66     i)
    67       IMAGES=images
    68       ;;
    69     t)
    70       TEST=test
    71       ;;
    72     \?)
    73       usage
    74       ;;
    75   esac
    76 done
    77 
    78 shift $(($OPTIND - 1))
    79 
    80 
    81 # args
    82 
    83 LOGICS="$@"
    84 
    85 [ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
    86 [ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
    87 
    88 
    89 ## main
    90 
    91 # tell the user about current values
    92 
    93 if [ -z "$BATCH" ]; then
    94   echo
    95   echo "                *****************************"
    96   echo "                * Welcome to Isabelle build *"
    97   echo "                *****************************"
    98   echo
    99   echo "Please check $ISABELLE_HOME/etc/settings"
   100   [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
   101   echo "to make sure that Isabelle's ML system settings and compilation options"
   102   echo "are appropriate."
   103   echo
   104   echo "The current values are:"
   105   echo
   106   echo "  ML_SYSTEM=$ML_SYSTEM"
   107   echo "  ML_HOME=$ML_HOME"
   108   echo "  ML_OPTIONS=$ML_OPTIONS"
   109   echo "  ML_PLATFORM=$ML_PLATFORM"
   110   echo
   111   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   112 fi
   113 
   114 
   115 # check logics
   116 
   117 if [ -z "$BATCH" ]; then
   118   echo
   119   echo
   120   echo "Press RETURN to start compilation (including parents) of:"
   121   echo
   122 fi
   123 
   124 
   125 MAKE_LOGICS=""
   126 
   127 for L in $LOGICS
   128 do
   129   DIR=$ISABELLE_HOME/src/$L
   130   if [ -f $DIR/IsaMakefile ]; then
   131     MAKE_LOGICS="$MAKE_LOGICS $L"
   132   else
   133     echo "No such logic: $L"
   134   fi
   135 done
   136 
   137 
   138 if [ -z "$BATCH" ]; then
   139   echo " " $MAKE_LOGICS
   140   echo
   141   read
   142 else
   143   echo
   144   echo "Isabelle build:" $MAKE_LOGICS
   145   echo
   146   echo "ML_SYSTEM=$ML_SYSTEM"
   147   echo "ML_HOME=$ML_HOME"
   148   echo "ML_OPTIONS=$ML_OPTIONS"
   149   echo
   150   echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   151   echo
   152 fi
   153 
   154 
   155 # build it
   156 
   157 SECONDS=0
   158 DATE=$(date)
   159 HOST=$(hostname)
   160 echo "Started at $DATE ($HOST)"
   161 
   162 export THIS_IS_ISABELLE_BUILD=true
   163 
   164 for L in $MAKE_LOGICS
   165 do
   166   ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $IMAGES $TEST )
   167 done
   168 
   169 echo -n "Finished at "; date
   170 
   171 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
   172 echo "$ELAPSED total elapsed time"