Admin/makebin

added option to Mirabelle/Sledgehammer

#!/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"