src/Pure/build

maintain set of source digests, including relevant parts of session entry;

#!/usr/bin/env bash
#
# Author: Makarius
#
# build - build Isabelle/ML
#
# Requires proper Isabelle settings environment.


## diagnostics

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] TARGET"
  echo
  echo "  Options are:"
  echo "    -b           build target images"
  echo
  echo "  Build Isabelle/ML TARGET: RAW or Pure"
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"


## process command line

# options

BUILD_IMAGES=false

while getopts "b" OPT
do
  case "$OPT" in
    b)
      BUILD_IMAGES="true"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

TARGET="Pure"
[ "$#" -ge 1 ] && { TARGET="$1"; shift; }
[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""

[ "$#" -eq 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\"!"


# run isabelle

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

if [ "$TARGET" = RAW ]; then
  if [ "$BUILD_IMAGES" = false ]; then
    "$ISABELLE_PROCESS" \
      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
      -q RAW_ML_SYSTEM
  else
    "$ISABELLE_PROCESS" \
      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
      -e "structure Isar = struct fun main () = () end;" \
      -e "ml_prompts \"ML> \" \"ML# \";" \
      -q -w RAW_ML_SYSTEM RAW
  fi
else
  if [ "$BUILD_IMAGES" = false ]; then
    "$ISABELLE_PROCESS" \
      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
      -q RAW_ML_SYSTEM
  else
    "$ISABELLE_PROCESS" \
      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
      -e "ml_prompts \"ML> \" \"ML# \";" \
      -f -q -w RAW_ML_SYSTEM Pure
  fi
fi

RC="$?"

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

if [ "$RC" -eq 0 ]; then
  echo "Finished $TARGET ($TIMES_REPORT)" >&2
fi

exit "$RC"