#!/usr/bin/env bash

#

# makebin -- make Isabelle logic images for current platform

## global settings

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

## diagnostics

PRG=$(basename "$0")

function usage()

{

  echo

  echo "Usage: $PRG [OPTIONS] ARCHIVE"

  echo

  echo "  Options are:"

  echo "    -l           produce library"

  echo

  echo "  Precompile Isabelle for the current platform."

  echo

  exit 1

}

function fail()

{

  echo "$1" >&2

  exit 2

}

## process command line

# options

DO_LIBRARY=""

while getopts "l" OPT

do

  case "$OPT" in

    l)

      DO_LIBRARY=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":;' \

  etc/settings

if [ -n "$DO_LIBRARY" ]; then

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

    etc/settings

fi

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

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

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

if [ -n "$DO_LIBRARY" ]; then

  ./build -bait -m all

else

  ./build -b HOL

fi

# prepare result

cd "$TMP"

chmod -R g=o "$TMP"

chgrp -R isabelle "$TMP"

if [ -n "$DO_LIBRARY" ]; then

  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"

else

  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"

fi

# clean up

rm -rf "$TMP"