# HG changeset patch # User wenzelm # Date 1344420814 -7200 # Node ID 519b6e53179b33446f0d26e9b81ee5114694aab9 # Parent 093eb27374bb475dc8ca7d7be694500c5cfd4151 obsolete; diff -r 093eb27374bb -r 519b6e53179b src/Pure/mk --- 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"