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