Admin/makebin

simplification of the Isabelle-ATP code; hooks for batch generation of problems

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


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

# FIXME: ugly hack to get proper HOL4 image
# needs HOL4 proof terms installed in ~/isabelle/proofs
# desperately needs fix for next release!
cat > src/HOL/Import/HOL/ROOT.ML <<EOF
with_path ".." use_thy "HOL4Compat";
with_path ".." use_thy "HOL4Syntax";
use_thy "HOL4Prob";
use_thy "HOL4";
EOF

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/HOL4"
  touch "heaps/$COMPILER/log/HOL4.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
  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 1"/' \
    etc/settings
  ./build -b -m HOL4 HOL
  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 HOL4 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"