src/Pure/mk
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15790 e68dab670fc5
child 16131 e1b85512d87d
permissions -rwxr-xr-x
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     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 "    -C           tell ML system to copy output image"
    21   echo "    -r           prepare RAW image only"
    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 COPY=""
    38 RAW=""
    39 
    40 while getopts "Cr" OPT
    41 do
    42   case "$OPT" in
    43     C)
    44       COPY="-C"
    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" ] && \
    69   fail "Missing ML system settings! Probably not run via 'isatool make'."
    70 
    71 COMPAT=""
    72 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
    73 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
    74 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    75 
    76 
    77 # prepare log dir
    78 
    79 LOGDIR="$ISABELLE_OUTPUT/log"
    80 mkdir -p "$LOGDIR"
    81 
    82 
    83 # run isabelle
    84 
    85 SECONDS=0
    86 
    87 if [ -z "$RAW" ]; then
    88   ITEM="Pure"
    89   echo "Building $ITEM ..."
    90   LOG="$LOGDIR/$ITEM"
    91 
    92   "$ISABELLE" $COPY \
    93     -e "val ml_system = \"$ML_SYSTEM\";" \
    94     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
    95     -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
    96   RC="$?"
    97 else
    98   ITEM="RAW"
    99   echo "Building $ITEM ..."
   100   LOG="$LOGDIR/$ITEM"
   101 
   102   "$ISABELLE" $COPY \
   103     -e "val ml_system = \"$ML_SYSTEM\";" \
   104     -e "use\"$COMPAT\" handle _ => exit 1;" \
   105     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
   106   RC="$?"
   107 fi
   108 
   109 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
   110 
   111 
   112 # exit status
   113 
   114 if [ "$RC" -eq 0 ]; then
   115   echo "Finished $ITEM ($ELAPSED elapsed time)"
   116   gzip --force "$LOG"
   117 else
   118   echo "$ITEM FAILED"
   119   echo "(see also $LOG)"
   120   echo; tail "$LOG"; echo
   121 fi
   122 
   123 exit "$RC"