wenzelm@11391: #!/usr/bin/env bash wenzelm@2339: # wenzelm@2339: # $Id$ wenzelm@9789: # Author: Markus Wenzel, TU Muenchen wenzelm@9789: # License: GPL (GNU GENERAL PUBLIC LICENSE) wenzelm@2339: # wenzelm@2339: # mk - build Pure Isabelle. wenzelm@2339: # wenzelm@10102: # Requires proper Isabelle settings environment (cf. IsaMakefile). wenzelm@2339: wenzelm@2339: wenzelm@2339: ## diagnostics wenzelm@2339: wenzelm@3774: function usage() wenzelm@3774: { wenzelm@3774: echo wenzelm@3774: echo "Usage: $PRG [OPTIONS]" wenzelm@3774: echo wenzelm@3774: echo " Make Pure Isabelle." wenzelm@3774: echo wenzelm@10102: echo " -C tell ML system to copy output image" wenzelm@10102: echo " -r prepare RAW image only" wenzelm@3774: echo wenzelm@3774: exit 1 wenzelm@3774: } wenzelm@3774: wenzelm@2339: function fail() wenzelm@2339: { wenzelm@2339: echo "$1" >&2 wenzelm@2339: exit 2 wenzelm@2339: } wenzelm@2339: wenzelm@2339: wenzelm@3774: ## process command line wenzelm@3774: wenzelm@3774: # options wenzelm@3774: wenzelm@10102: COPY="" wenzelm@3774: RAW="" wenzelm@3774: wenzelm@10102: while getopts "Cr" OPT wenzelm@3774: do wenzelm@3774: case "$OPT" in wenzelm@10102: C) wenzelm@10102: COPY="-C" wenzelm@10102: ;; wenzelm@3774: r) wenzelm@3774: RAW=true wenzelm@3774: ;; wenzelm@3774: \?) wenzelm@3774: usage wenzelm@3774: ;; wenzelm@3774: esac wenzelm@3774: done wenzelm@3774: wenzelm@3774: shift $(($OPTIND - 1)) wenzelm@3774: wenzelm@3774: wenzelm@3774: # args wenzelm@3774: wenzelm@9789: [ "$#" -ne 0 ] && usage wenzelm@3774: wenzelm@3774: wenzelm@2339: ## main wenzelm@2339: wenzelm@4442: # get compatibility file wenzelm@4442: wenzelm@9789: ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) wenzelm@3056: [ -z "$ML_SYSTEM" ] && \ wenzelm@6186: fail "Missing ML system settings! Probably not run via 'isatool make'." wenzelm@2339: wenzelm@2339: COMPAT="" wenzelm@2339: [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML" wenzelm@2339: [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML" wenzelm@2339: [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" wenzelm@2339: wenzelm@4442: wenzelm@4442: # prepare log dir wenzelm@4442: wenzelm@4442: LOGDIR="$ISABELLE_OUTPUT/log" wenzelm@4442: mkdir -p "$LOGDIR" wenzelm@4442: wenzelm@4442: wenzelm@4442: # run isabelle wenzelm@4442: wenzelm@4442: SECONDS=0 wenzelm@4442: wenzelm@3774: if [ -z "$RAW" ]; then wenzelm@4442: ITEM="Pure" wenzelm@7277: echo "Building $ITEM ..." wenzelm@4442: LOG="$LOGDIR/$ITEM" wenzelm@4442: wenzelm@10102: "$ISABELLE" $COPY \ wenzelm@3774: -e "val ml_system = \"$ML_SYSTEM\";" \ wenzelm@4495: -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ wenzelm@10900: -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 wenzelm@9789: RC="$?" wenzelm@3774: else wenzelm@4442: ITEM="RAW" wenzelm@7277: echo "Building $ITEM ..." wenzelm@4442: LOG="$LOGDIR/$ITEM" wenzelm@4442: wenzelm@10102: "$ISABELLE" $COPY \ wenzelm@3774: -e "val ml_system = \"$ML_SYSTEM\";" \ wenzelm@10900: -e "use\"$COMPAT\" handle _ => exit 1;" \ wenzelm@9789: -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 wenzelm@9789: RC="$?" wenzelm@3774: fi wenzelm@4442: wenzelm@9789: ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") wenzelm@4442: wenzelm@4442: wenzelm@4442: # exit status wenzelm@4442: wenzelm@9789: if [ "$RC" -eq 0 ]; then wenzelm@7277: echo "Finished $ITEM ($ELAPSED elapsed time)" wenzelm@4442: gzip --force "$LOG" wenzelm@4442: else wenzelm@7263: echo "$ITEM FAILED" wenzelm@4442: echo "(see also $LOG)" wenzelm@9789: echo; tail "$LOG"; echo wenzelm@4442: fi wenzelm@4442: wenzelm@9789: exit "$RC"