#!/usr/bin/env bash

#

# $Id$

#

# makebin -- make Isabelle logic images for current platform.

## global settings

DISTBASE=~/tmp/isadist

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

TAR=tar

type -path gtar >/dev/null && TAR=gtar

export THIS_IS_ISABELLE_BUILD=true

export THIS_IS_ISABELLE_ADMIN=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"

if [ -n "$DO_LIBRARY" ]; then

  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \

    etc/settings

else

  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \

    etc/settings

fi

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

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

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

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

PLATFORM=$(./bin/isatool 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-Complex"

  touch "heaps/$COMPILER/log/HOL-Complex.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-Complex HOL

  ./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-Complex 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"