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