src/Pure/mk
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 34282 549969a7f582
child 43948 8f5add916a99
permissions -rwxr-xr-x
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     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 "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 -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"