build
author wenzelm
Wed Apr 02 19:12:26 1997 +0200 (1997-04-02 ago)
changeset 2879 477bfcb022d8
parent 2789 69cf3aea45ee
child 2902 bacef535265c
permissions -rwxr-xr-x
misc improvements;
     1 #!/bin/bash -norc
     2 #
     3 # $Id$
     4 #
     5 # build - compile parts of the Isabelle system
     6 
     7 
     8 ## settings
     9 
    10 PRG=$(basename $0)
    11 
    12 ISABELLE_HOME=$(dirname $0)
    13 . $ISABELLE_HOME/lib/scripts/getsettings || \
    14   { echo "$PRG probably not called from its original place!"; exit 2 }
    15 
    16 
    17 ## diagnostics
    18 
    19 function usage()
    20 {
    21   echo
    22   echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
    23   echo
    24   echo "  Options are:"
    25   echo "    -a           all logics"
    26   echo
    27   echo "  Compile the named LOGICS (default $DEFAULT_LOGIC), or all object logics"
    28   echo "  in the distribution."
    29   echo
    30   exit 1
    31 }
    32 
    33 function fail()
    34 {
    35   echo "$1" >&2
    36   exit 2
    37 }
    38 
    39 
    40 ## process command line
    41 
    42 # options
    43 
    44 ALL=""
    45 
    46 while getopts "a" OPT
    47 do
    48   case "$OPT" in
    49     a)
    50       ALL=true
    51       ;;
    52     \?)
    53       usage
    54       ;;
    55   esac
    56 done
    57 
    58 shift $(($OPTIND - 1))
    59 
    60 
    61 # args
    62 
    63 LOGICS="$@"
    64 
    65 
    66 ## main
    67 
    68 # tell the user about current values
    69 
    70 echo
    71 echo "                *****************************"
    72 echo "                * Welcome to Isabelle build *"
    73 echo "                *****************************"
    74 echo
    75 echo "Please check $ISABELLE_HOME/etc/settings"
    76 [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
    77 echo "to make sure that Isabelle's ML system settings are appropriate."
    78 echo
    79 echo "Your current values are:"
    80 echo
    81 
    82 echo "  ML_SYSTEM=$ML_SYSTEM"
    83 echo "  ML_HOME=$ML_HOME"
    84 echo "  ML_OPTIONS=$ML_OPTIONS"
    85 
    86 
    87 # check logics
    88 
    89 echo
    90 echo
    91 echo "Press RETURN to start compilation (including parents) of:"
    92 echo
    93 
    94 [ -z "$LOGICS" ] && LOGICS=$DEFAULT_LOGIC
    95 
    96 if [ -n "$ALL" ]; then
    97   LOGICS=""
    98   for DIR in $ISABELLE_HOME/src/*
    99   do
   100     if [ -f $DIR/IsaMakefile ]; then
   101       L=$(basename $DIR)
   102       LOGICS="$LOGICS $L"
   103     fi
   104   done
   105 else
   106   for L in $LOGICS
   107   do
   108     DIR=$ISABELLE_HOME/src/$L
   109     [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
   110   done
   111 fi
   112 
   113 echo " " $LOGICS
   114 echo
   115 read
   116 
   117 
   118 # build it
   119 
   120 export THIS_IS_ISABELLE_BUILD=true
   121 
   122 for L in $LOGICS
   123 do
   124   ( cd $ISABELLE_HOME/src/$L; $ISATOOL make )
   125 done