src/Pure/mk

split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)

#!/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 "val ml_system = \"$ML_SYSTEM\";" \
    -e "val ml_platform = \"$ML_PLATFORM\";" \
    -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 "val ml_system = \"$ML_SYSTEM\";" \
    -e "val ml_platform = \"$ML_PLATFORM\";" \
    -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"