#!/bin/bash
#
# $Id$
#
# makebin -- make Isabelle logic images for current platform.
## global settings
FAKE_BUILD=""
DISTBASE=~/tmp/isadist
TMP="/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 ARCHIVE"
echo
echo " Make Isabelle logic images for current platform."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
[ "$#" -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"
#activate default for precompiled distribution ...
perl -pi -e 's/#ISABELLE_USEDIR_OPTIONS/ISABELLE_USEDIR_OPTIONS/' etc/settings
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 "$FAKE_BUILD" ]; then
mkdir -p "heaps/$COMPILER"
touch "heaps/$COMPILER/HOL"
touch "heaps/$COMPILER/HOL-Real"
touch "heaps/$COMPILER/ZF"
else
./build -b -m HOL-Real 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"
for IMG in HOL HOL-Real ZF
do
"$TAR" cf "${IMG}_$PLATFORM.tar" \
"$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
"$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
gzip "${IMG}_$PLATFORM.tar"
cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
done
# clean up
cd /tmp
rm -rf "$TMP"