src/Pure/mk
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 43948 8f5add916a99
permissions -rwxr-xr-x
more official command specifications, including source position;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # mk - build Isabelle/Pure.
     6 #
     7 # Requires proper Isabelle settings environment.
     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 "use\"$COMPAT\" handle _ => exit 1;" \
    92     -e "structure Isar = struct fun main () = () end;" \
    93     -e "ml_prompts \"ML> \" \"ML# \";" \
    94     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
    95   RC="$?"
    96 elif [ -n "$RAW_SESSION" ]; then
    97   ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
    98   echo "Running $ITEM ..."
    99   LOG="$LOGDIR/$ITEM"
   100 
   101   "$ISABELLE_PROCESS" \
   102     -e "use\"$RAW_SESSION\" handle _ => exit 1;" \
   103     -q RAW > "$LOG" 2>&1
   104   RC="$?"
   105 else
   106   ITEM="Pure"
   107   echo "Building $ITEM ..."
   108   LOG="$LOGDIR/$ITEM"
   109 
   110   "$ISABELLE_PROCESS" \
   111     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
   112     -e "ml_prompts \"ML> \" \"ML# \";" \
   113     -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   114   RC="$?"
   115 fi
   116 
   117 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   118 
   119 
   120 # exit status
   121 
   122 if [ "$RC" -eq 0 ]; then
   123   echo "Finished $ITEM ($TIMES_REPORT)"
   124   gzip --force "$LOG"
   125 else
   126   echo "$ITEM FAILED"
   127   echo "(see also $LOG)"
   128   echo; tail "$LOG"; echo
   129 fi
   130 
   131 exit "$RC"