Admin/makebin

A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.

#!/usr/bin/env bash
#
# $Id$
#
# makebin -- make Isabelle logic images for current platform.


## global settings

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

perl -pi \
  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
  etc/settings

if [ -n "$DO_LIBRARY" ]; then
  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
    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 -m HOL4 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 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"