#!/usr/bin/env bash
#
# makebundle -- re-package with add-on components
## diagnostics
PRG=$(basename "$0")
function usage()
{
echo
echo "Usage: $PRG ARCHIVE PLATFORM"
echo
echo " Re-package Isabelle source distribution with add-on components"
echo " and logic images"
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## implicit and explicit arguments
TMP="/var/tmp/isabelle-makebundle$$"
mkdir "$TMP" || fail "Cannot create directory $TMP"
LOGICS="HOL HOL-Nominal HOLCF ZF"
[ "$#" -ne 2 ] && usage
ARCHIVE="$1"; shift
PLATFORM="$1"; shift
[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
## main
ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
tar -C "$TMP" -x -z -f "$ARCHIVE"
echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
for CONTRIB in "$ARCHIVE_DIR"/contrib/*.tar.gz
do
tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB"
NAME="$(basename "$CONTRIB" .tar.gz)"
[ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB"
if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
echo "component $NAME"
echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
else
echo "package $NAME"
fi
done
for LOGIC in $LOGICS
do
LOGIC_ARCHIVE="$ARCHIVE_DIR/${LOGIC}_${PLATFORM}.tar.gz"
[ -f "$LOGIC_ARCHIVE" ] || fail "Bad logic archive: $LOGIC_ARCHIVE"
echo "logic $LOGIC"
tar -C "$ISABELLE_HOME" -x -z -f "$LOGIC_ARCHIVE"
done
BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
echo "$(basename "$BUNDLE_ARCHIVE")"
tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" Isabelle "$ISABELLE_NAME"
# clean up
cd /tmp
rm -rf "$TMP"