#!/usr/bin/env bash
#
# build Isabelle HTML library from platform bundle
## diagnostics
PRG=$(basename "$0")
function usage()
{
echo
echo "Usage: $PRG [OPTIONS] ARCHIVE"
echo
echo " Options are:"
echo " -j INT maximum number of parallel jobs (default 1)"
echo
echo " Build Isabelle HTML library from platform bundle."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
JOBS=""
while getopts "j:" OPT
do
case "$OPT" in
j)
JOBS="-j $OPTARG"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
[ "$#" -ne 1 ] && usage
ARCHIVE="$1"; shift
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
ARCHIVE_BASE="$(basename "$ARCHIVE")"
ARCHIVE_DIR="$(cd "$(dirname "$ARCHIVE")"; echo "$PWD")"
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
## main
#GNU tar (notably on Mac OS X)
if [ -x /usr/bin/gnutar ]; then
function tar() { /usr/bin/gnutar "$@"; }
fi
TMP="/var/tmp/isabelle-makedist$$"
mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
cd "$TMP"
tar -x -z -f "$ARCHIVE_FULL"
cd *
ISABELLE_NAME="$(basename "$PWD")"
echo "ISABELLE_FULL_TEST=true" >> etc/settings
echo -n > src/Doc/ROOT
env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
./bin/isabelle build $JOBS -s -c -a -o browser_info \
-o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
RC="$?"
cd ..
if [ "$RC" = 0 ]; then
chmod -R a+r "$ISABELLE_NAME"
chmod -R g=o "$ISABELLE_NAME"
tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
fi
# clean up
cd /tmp
rm -rf "$TMP"
exit "$RC"