build
author wenzelm
Tue Dec 01 14:46:35 1998 +0100 (1998-12-01)
changeset 6000 aa84c30c1f61
parent 5393 7299e531d481
child 6256 e17fb80b3ce1
permissions -rwxr-xr-x
show_tags flag;
     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 "    -t           run tests"
    33   echo
    34   echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
    35   echo "  in the distribution."
    36   echo
    37   exit 1
    38 }
    39 
    40 function fail()
    41 {
    42   echo "$1" >&2
    43   exit 2
    44 }
    45 
    46 
    47 ## process command line
    48 
    49 # options
    50 
    51 ALL=""
    52 BATCH=""
    53 TEST=""
    54 
    55 while getopts "abt" OPT
    56 do
    57   case "$OPT" in
    58     a)
    59       ALL=true
    60       ;;
    61     b)
    62       BATCH=true
    63       ;;
    64     t)
    65       TEST=test
    66       ;;
    67     \?)
    68       usage
    69       ;;
    70   esac
    71 done
    72 
    73 shift $(($OPTIND - 1))
    74 
    75 
    76 # args
    77 
    78 LOGICS="$@"
    79 
    80 [ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
    81 [ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
    82 
    83 
    84 ## main
    85 
    86 # tell the user about current values
    87 
    88 if [ -z "$BATCH" ]; then
    89   echo
    90   echo "                *****************************"
    91   echo "                * Welcome to Isabelle build *"
    92   echo "                *****************************"
    93   echo
    94   echo "Please check $ISABELLE_HOME/etc/settings"
    95   [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
    96   echo "to make sure that Isabelle's ML system settings and compilation options"
    97   echo "are appropriate."
    98   echo
    99   echo "The current values are:"
   100   echo
   101   echo "  ML_SYSTEM=$ML_SYSTEM"
   102   echo "  ML_HOME=$ML_HOME"
   103   echo "  ML_OPTIONS=$ML_OPTIONS"
   104   echo
   105   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   106 fi
   107 
   108 
   109 # check logics
   110 
   111 if [ -z "$BATCH" ]; then
   112   echo
   113   echo
   114   echo "Press RETURN to start compilation (including parents) of:"
   115   echo
   116 fi
   117 
   118 
   119 MAKE_LOGICS=""
   120 
   121 for L in $LOGICS
   122 do
   123   DIR=$ISABELLE_HOME/src/$L
   124   if [ -f $DIR/IsaMakefile ]; then
   125     MAKE_LOGICS="$MAKE_LOGICS $L"
   126   else
   127     echo "No such logic: $L"
   128   fi
   129 done
   130 
   131 
   132 if [ -z "$BATCH" ]; then
   133   echo " " $MAKE_LOGICS
   134   echo
   135   read
   136 else
   137   echo
   138   echo "Isabelle build:" $MAKE_LOGICS
   139   echo
   140   echo "ML_SYSTEM=$ML_SYSTEM"
   141   echo "ML_HOME=$ML_HOME"
   142   echo "ML_OPTIONS=$ML_OPTIONS"
   143   echo
   144   echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   145   echo
   146 fi
   147 
   148 
   149 # build it
   150 
   151 SECONDS=0
   152 echo -n "Started at "; date
   153 
   154 export THIS_IS_ISABELLE_BUILD=true
   155 
   156 for L in $MAKE_LOGICS
   157 do
   158   ( cd $ISABELLE_HOME/src/$L; $ISATOOL make images $TEST )
   159 done
   160 
   161 echo -n "Finished at "; date
   162 
   163 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
   164 echo "$ELAPSED total elapsed time"