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