--- a/src/Pure/mk Wed Aug 08 12:10:22 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# mk - build Isabelle/Pure.
-#
-# Requires proper Isabelle settings environment.
-
-
-## diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG [OPTIONS]"
- echo
- echo " Make Pure Isabelle."
- echo
- echo " -R DIR/FILE run RAW session"
- echo " -r build RAW image"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-RAW_SESSION=""
-RAW=""
-
-while getopts "R:r" OPT
-do
- case "$OPT" in
- R)
- RAW_SESSION="$OPTARG"
- ;;
- r)
- RAW=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-# get compatibility file
-
-ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
-
-COMPAT=""
-[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
-[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
-[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
-
-
-# prepare log dir
-
-LOGDIR="$ISABELLE_OUTPUT/log"
-mkdir -p "$LOGDIR"
-
-
-# run isabelle
-
-. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-
-if [ -n "$RAW" ]; then
- ITEM="RAW"
- echo "Building $ITEM ..."
- LOG="$LOGDIR/$ITEM"
-
- "$ISABELLE_PROCESS" \
- -e "use\"$COMPAT\" handle _ => exit 1;" \
- -e "structure Isar = struct fun main () = () end;" \
- -e "ml_prompts \"ML> \" \"ML# \";" \
- -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
- RC="$?"
-elif [ -n "$RAW_SESSION" ]; then
- ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
- echo "Running $ITEM ..."
- LOG="$LOGDIR/$ITEM"
-
- "$ISABELLE_PROCESS" \
- -e "use\"$RAW_SESSION\" handle _ => exit 1;" \
- -q RAW > "$LOG" 2>&1
- RC="$?"
-else
- ITEM="Pure"
- echo "Building $ITEM ..."
- LOG="$LOGDIR/$ITEM"
-
- "$ISABELLE_PROCESS" \
- -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
- -e "ml_prompts \"ML> \" \"ML# \";" \
- -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
- RC="$?"
-fi
-
-. "$ISABELLE_HOME/lib/scripts/timestop.bash"
-
-
-# exit status
-
-if [ "$RC" -eq 0 ]; then
- echo "Finished $ITEM ($TIMES_REPORT)"
- gzip --force "$LOG"
-else
- echo "$ITEM FAILED"
- echo "(see also $LOG)"
- echo; tail "$LOG"; echo
-fi
-
-exit "$RC"