build
author wenzelm
Fri Dec 19 12:16:32 1997 +0100 (1997-12-19)
changeset 4457 6e6d99e06d0c
parent 3255 7678f3d93053
child 4581 52edf5ac3afa
permissions -rwxr-xr-x
tuned;
     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 are appropriate."
    97   echo
    98   echo "Your current values are:"
    99   echo
   100   echo "  ML_SYSTEM=$ML_SYSTEM"
   101   echo "  ML_HOME=$ML_HOME"
   102   echo "  ML_OPTIONS=$ML_OPTIONS"
   103 fi
   104 
   105 
   106 # check logics
   107 
   108 if [ -z "$BATCH" ]; then
   109   echo
   110   echo
   111   echo "Press RETURN to start compilation (including parents) of:"
   112   echo
   113 fi
   114 
   115 
   116 MAKE_LOGICS=""
   117 
   118 for L in $LOGICS
   119 do
   120   DIR=$ISABELLE_HOME/src/$L
   121   if [ -f $DIR/IsaMakefile ]; then
   122     MAKE_LOGICS="$MAKE_LOGICS $L"
   123   else
   124     echo "No such logic: $L"
   125   fi
   126 done
   127 
   128 
   129 if [ -z "$BATCH" ]; then
   130   echo " " $MAKE_LOGICS
   131   echo
   132   read
   133 else
   134   echo
   135   echo "Isabelle build:" $MAKE_LOGICS
   136   echo
   137   echo "ML_SYSTEM=$ML_SYSTEM"
   138   echo "ML_HOME=$ML_HOME"
   139   echo "ML_OPTIONS=$ML_OPTIONS"
   140   echo
   141 fi
   142 
   143 
   144 # build it
   145 
   146 SECONDS=0
   147 echo -n "Started at "; date
   148 
   149 export THIS_IS_ISABELLE_BUILD=true
   150 
   151 for L in $MAKE_LOGICS
   152 do
   153   ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TEST )
   154 done
   155 
   156 echo -n "Finished at "; date
   157 
   158 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
   159 echo "$ELAPSED total elapsed time"