src/Pure/mk
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 28502 6b0e3e4e1891
child 30204 8ede2f7104cf
permissions -rwxr-xr-x
use long names for old-style fold combinators;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 #
     6 # mk - build Pure Isabelle.
     7 #
     8 # Requires proper Isabelle settings environment (cf. IsaMakefile).
     9 
    10 
    11 ## diagnostics
    12 
    13 function usage()
    14 {
    15   echo
    16   echo "Usage: $PRG [OPTIONS]"
    17   echo
    18   echo "  Make Pure Isabelle."
    19   echo
    20   echo "    -R DIR/FILE  run RAW session"
    21   echo "    -r           build RAW image"
    22   echo
    23   exit 1
    24 }
    25 
    26 function fail()
    27 {
    28   echo "$1" >&2
    29   exit 2
    30 }
    31 
    32 
    33 ## process command line
    34 
    35 # options
    36 
    37 RAW_SESSION=""
    38 RAW=""
    39 
    40 while getopts "R:r" OPT
    41 do
    42   case "$OPT" in
    43     R)
    44       RAW_SESSION="$OPTARG"
    45       ;;
    46     r)
    47       RAW=true
    48       ;;
    49     \?)
    50       usage
    51       ;;
    52   esac
    53 done
    54 
    55 shift $(($OPTIND - 1))
    56 
    57 
    58 # args
    59 
    60 [ "$#" -ne 0 ] && usage
    61 
    62 
    63 ## main
    64 
    65 # get compatibility file
    66 
    67 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
    68 [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
    69 
    70 COMPAT=""
    71 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
    72 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
    73 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    74 
    75 
    76 # prepare log dir
    77 
    78 LOGDIR="$ISABELLE_OUTPUT/log"
    79 mkdir -p "$LOGDIR"
    80 
    81 
    82 # run isabelle
    83 
    84 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    85 
    86 if [ -n "$RAW" ]; then
    87   ITEM="RAW"
    88   echo "Building $ITEM ..."
    89   LOG="$LOGDIR/$ITEM"
    90 
    91   "$ISABELLE_PROCESS" \
    92     -e "val ml_system = \"$ML_SYSTEM\";" \
    93     -e "val ml_platform = \"$ML_PLATFORM\";" \
    94     -e "use\"$COMPAT\" handle _ => exit 1;" \
    95     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
    96   RC="$?"
    97 elif [ -n "$RAW_SESSION" ]; then
    98   ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
    99   echo "Running $ITEM ..."
   100   LOG="$LOGDIR/$ITEM"
   101 
   102   "$ISABELLE_PROCESS" \
   103     -e "use\"$RAW_SESSION\" handle _ => exit 1;" \
   104     -q RAW > "$LOG" 2>&1
   105   RC="$?"
   106 else
   107   ITEM="Pure"
   108   echo "Building $ITEM ..."
   109   LOG="$LOGDIR/$ITEM"
   110 
   111   "$ISABELLE_PROCESS" \
   112     -e "val ml_system = \"$ML_SYSTEM\";" \
   113     -e "val ml_platform = \"$ML_PLATFORM\";" \
   114     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
   115     -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   116   RC="$?"
   117 fi
   118 
   119 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   120 
   121 
   122 # exit status
   123 
   124 if [ "$RC" -eq 0 ]; then
   125   echo "Finished $ITEM ($TIMES_REPORT)"
   126   gzip --force "$LOG"
   127 else
   128   echo "$ITEM FAILED"
   129   echo "(see also $LOG)"
   130   echo; tail "$LOG"; echo
   131 fi
   132 
   133 exit "$RC"