isabelle: src/Pure/mk@72abe86d9418

     1 #!/bin/bash

2 #

     3 # $Id$

4 #

     5 # mk - build Pure Isabelle.

6 #

     7 # Assumes to be called via Isabelle make utility (cf. IsaMakefile).

    10 ## diagnostics

    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 }

    24 function fail()

    25 {

    26   echo "$1" >&2

    27   exit 2

    28 }

    31 ## process command line

    33 # options

    35 RAW=""

    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

    49 shift $(($OPTIND - 1))

    52 # args

    54 [ $# -ne 0 ] && usage

    57 ## main

    59 # get compatibility file

    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'."

    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\"!"

    71 # prepare log dir

    73 LOGDIR="$ISABELLE_OUTPUT/log"

    74 mkdir -p "$LOGDIR"

    77 # run isabelle

    79 SECONDS=0

    81 if [ -z "$RAW" ]; then

    82   ITEM="Pure"

    83   echo -n "Building $ITEM ... "

    84   LOG="$LOGDIR/$ITEM"

    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 else

    91   ITEM="RAW"

    92   echo -n "Building $ITEM ... "

    93   LOG="$LOGDIR/$ITEM"

    95   $ISABELLE \

    96     -e "val ml_system = \"$ML_SYSTEM\";" \

    97     -e "use\"$COMPAT\" handle _ => exit 1;;" \

    98     -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1

    99 fi

   101 RC=$?

   103 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)

   106 # exit status

   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

   117 exit $RC

author	wenzelm
	Wed Feb 03 16:41:00 1999 +0100 (1999-02-03)
changeset 6186	72abe86d9418
parent 4495	8648ba842d14
child 6239	6b9194aff620
permissions	-rwxr-xr-x