src/Pure/mk
author berghofe
Wed Oct 31 19:37:04 2001 +0100 (2001-10-31)
changeset 11998 b14e7686ce84
parent 11391 e8638d07fdee
child 14981 e73f8140af78
permissions -rwxr-xr-x
- enter_thmx -> enter_thms
- improved naming of theorems: enter_thms now takes functions pre_name and post_name
as arguments
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # mk - build Pure Isabelle.
     8 #
     9 # Requires proper Isabelle settings environment (cf. IsaMakefile).
    10 
    11 
    12 ## diagnostics
    13 
    14 function usage()
    15 {
    16   echo
    17   echo "Usage: $PRG [OPTIONS]"
    18   echo
    19   echo "  Make Pure Isabelle."
    20   echo
    21   echo "    -C           tell ML system to copy output image"
    22   echo "    -r           prepare RAW image only"
    23   echo
    24   exit 1
    25 }
    26 
    27 function fail()
    28 {
    29   echo "$1" >&2
    30   exit 2
    31 }
    32 
    33 
    34 ## process command line
    35 
    36 # options
    37 
    38 COPY=""
    39 RAW=""
    40 
    41 while getopts "Cr" OPT
    42 do
    43   case "$OPT" in
    44     C)
    45       COPY="-C"
    46       ;;
    47     r)
    48       RAW=true
    49       ;;
    50     \?)
    51       usage
    52       ;;
    53   esac
    54 done
    55 
    56 shift $(($OPTIND - 1))
    57 
    58 
    59 # args
    60 
    61 [ "$#" -ne 0 ] && usage
    62 
    63 
    64 ## main
    65 
    66 # get compatibility file
    67 
    68 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
    69 [ -z "$ML_SYSTEM" ] && \
    70   fail "Missing ML system settings! Probably not run via 'isatool make'."
    71 
    72 COMPAT=""
    73 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
    74 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
    75 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    76 
    77 
    78 # prepare log dir
    79 
    80 LOGDIR="$ISABELLE_OUTPUT/log"
    81 mkdir -p "$LOGDIR"
    82 
    83 
    84 # run isabelle
    85 
    86 SECONDS=0
    87 
    88 if [ -z "$RAW" ]; then
    89   ITEM="Pure"
    90   echo "Building $ITEM ..."
    91   LOG="$LOGDIR/$ITEM"
    92 
    93   "$ISABELLE" $COPY \
    94     -e "val ml_system = \"$ML_SYSTEM\";" \
    95     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
    96     -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
    97   RC="$?"
    98 else
    99   ITEM="RAW"
   100   echo "Building $ITEM ..."
   101   LOG="$LOGDIR/$ITEM"
   102 
   103   "$ISABELLE" $COPY \
   104     -e "val ml_system = \"$ML_SYSTEM\";" \
   105     -e "use\"$COMPAT\" handle _ => exit 1;" \
   106     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
   107   RC="$?"
   108 fi
   109 
   110 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
   111 
   112 
   113 # exit status
   114 
   115 if [ "$RC" -eq 0 ]; then
   116   echo "Finished $ITEM ($ELAPSED elapsed time)"
   117   gzip --force "$LOG"
   118 else
   119   echo "$ITEM FAILED"
   120   echo "(see also $LOG)"
   121   echo; tail "$LOG"; echo
   122 fi
   123 
   124 exit "$RC"