src/Pure/mk
author wenzelm
Thu Jul 08 18:31:04 1999 +0200 (1999-07-08)
changeset 6930 4b40fb299f9f
parent 6239 6b9194aff620
child 7263 2d09363ada6c
permissions -rwxr-xr-x
improved error msgs of cterm_instantiate;
fixed incr_indexes;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # mk - build Pure Isabelle.
     6 #
     7 # Assumes to be called via Isabelle make utility (cf. IsaMakefile).
     8 
     9 
    10 ## diagnostics
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [OPTIONS]"
    16   echo
    17   echo "  Make Pure Isabelle."
    18   echo
    19   echo "    -r           just prepare RAW image"
    20   echo
    21   exit 1
    22 }
    23 
    24 function fail()
    25 {
    26   echo "$1" >&2
    27   exit 2
    28 }
    29 
    30 
    31 ## process command line
    32 
    33 # options
    34 
    35 RAW=""
    36 
    37 while getopts "r" OPT
    38 do
    39   case "$OPT" in
    40     r)
    41       RAW=true
    42       ;;
    43     \?)
    44       usage
    45       ;;
    46   esac
    47 done
    48 
    49 shift $(($OPTIND - 1))
    50 
    51 
    52 # args
    53 
    54 [ $# -ne 0 ] && usage
    55 
    56 
    57 ## main
    58 
    59 # get compatibility file
    60 
    61 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
    62 [ -z "$ML_SYSTEM" ] && \
    63   fail "Missing ML system settings! Probably not run via 'isatool make'."
    64 
    65 COMPAT=""
    66 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
    67 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
    68 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    69 
    70 
    71 # prepare log dir
    72 
    73 LOGDIR="$ISABELLE_OUTPUT/log"
    74 mkdir -p "$LOGDIR"
    75 
    76 
    77 # run isabelle
    78 
    79 SECONDS=0
    80 
    81 if [ -z "$RAW" ]; then
    82   ITEM="Pure"
    83   echo -n "Building $ITEM ... "
    84   LOG="$LOGDIR/$ITEM"
    85 
    86   $ISABELLE \
    87     -e "val ml_system = \"$ML_SYSTEM\";" \
    88     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
    89     -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1
    90   RC=$?
    91 else
    92   ITEM="RAW"
    93   echo -n "Building $ITEM ... "
    94   LOG="$LOGDIR/$ITEM"
    95 
    96   $ISABELLE \
    97     -e "val ml_system = \"$ML_SYSTEM\";" \
    98     -e "use\"$COMPAT\" handle _ => exit 1;;" \
    99     -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1
   100   RC=$?
   101 fi
   102 
   103 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
   104 
   105 
   106 # exit status
   107 
   108 if [ $RC -eq 0 ]; then
   109   echo "OK  ($ELAPSED elapsed time)"
   110   gzip --force "$LOG"
   111 else
   112   echo "FAILED"
   113   echo "(see also $LOG)"
   114   echo; tail $LOG; echo
   115 fi
   116 
   117 exit $RC