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