wneuper/isa: src/Pure/mk@0d95980e9aae

     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.

    10 ## diagnostics

    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 }

    25 function fail()

    26 {

    27   echo "$1" >&2

    28   exit 2

    29 }

    32 ## process command line

    34 # options

    36 RAW_SESSION=""

    37 RAW=""

    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

    54 shift $(($OPTIND - 1))

    57 # args

    59 [ "$#" -ne 0 ] && usage

    62 ## main

    64 # get compatibility file

    66 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)

    67 [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"

    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\"!"

    75 # prepare log dir

    77 LOGDIR="$ISABELLE_OUTPUT/log"

    78 mkdir -p "$LOGDIR"

    81 # run isabelle

    83 . "$ISABELLE_HOME/lib/scripts/timestart.bash"

    85 if [ -n "$RAW" ]; then

    86   ITEM="RAW"

    87   echo "Building $ITEM ..."

    88   LOG="$LOGDIR/$ITEM"

    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"

   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"

   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

   117 . "$ISABELLE_HOME/lib/scripts/timestop.bash"

   120 # exit status

   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

   131 exit "$RC"

author	wenzelm
	Sun, 22 Jul 2012 23:31:57 +0200
changeset 49440	0d95980e9aae
parent 44819	8f5add916a99
permissions	-rwxr-xr-x