#!/usr/bin/env bash

#

# makebin -- make Isabelle logic images for current platform

## global settings

TMP="/var/tmp/isabelle-makebin$$"

export THIS_IS_ISABELLE_MAKEBIN=true

## diagnostics

PRG=$(basename "$0")

function usage()

{

  echo

  echo "Usage: $PRG [OPTIONS] ARCHIVE"

  echo

  echo "  Options are:"

  echo "    -l           produce library"

  echo "    -n           dry run"

  echo

  echo "  Precompile Isabelle for the current platform."

  echo

  exit 1

}

function fail()

{

  echo "$1" >&2

  exit 2

}

## process command line

# options

DO_LIBRARY=""

DRY_RUN=""

while getopts "ln" OPT

do

  case "$OPT" in

    l)

      DO_LIBRARY=true

      ;;

    n)

      DRY_RUN=true

      ;;

    \?)

      usage

      ;;

  esac

done

shift $(($OPTIND - 1))

# args

[ "$#" -gt 1 ] && usage

ARCHIVE="$1"; shift

## main

[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"

ARCHIVE_BASE="$(basename "$ARCHIVE")"

ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"

ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"

ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"

ISABELLE_HOME="$TMP/$ISABELLE_NAME"

# build logics

mkdir "$TMP" || fail "Cannot create directory $TMP"

cd "$TMP"

tar xzf "$ARCHIVE_FULL"

cd "$ISABELLE_NAME"

perl -pi \

  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \

  etc/settings

if [ -n "$DO_LIBRARY" ]; then

  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \

    etc/settings

fi

ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)

[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \

  echo "### WARNING!  Personal Isabelle settings present. " >&2

COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)

PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)

if [ -n "$DRY_RUN" ]; then

  mkdir -p "heaps/$COMPILER/log"

  touch "heaps/$COMPILER/HOL"

  touch "heaps/$COMPILER/log/HOL.gz"

  touch "heaps/$COMPILER/HOL-Nominal"

  touch "heaps/$COMPILER/log/HOL-Nominal.gz"

  touch "heaps/$COMPILER/HOLCF"

  touch "heaps/$COMPILER/log/HOLCF.gz"

  touch "heaps/$COMPILER/ZF"

  touch "heaps/$COMPILER/log/ZF.gz"

  mkdir browser_info

elif [ -n "$DO_LIBRARY" ]; then

  ./build -bait

else

  ./build -b -m HOL-Nominal HOL

  ./build -b HOLCF

  ./build -b ZF

  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"

fi

# prepare result

cd "$TMP"

chmod -R g=o "$TMP"

chgrp -R isabelle "$TMP"

if [ -n "$DO_LIBRARY" ]; then

  tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \

    gzip -f "${ISABELLE_NAME}_library.tar"

    cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"

else

  for IMG in HOL HOL-Nominal HOLCF ZF

  do

    tar cf "${IMG}_$PLATFORM.tar" \

      "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \

      "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"

    gzip -f "${IMG}_$PLATFORM.tar"

    cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"

  done

fi

# clean up

cd /tmp

rm -rf "$TMP"