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