#!/usr/bin/env bash
#
# Author: Makarius
#
# build full Isabelle distribution from repository
THIS="$(cd "$(dirname "$0")"; pwd)"
PRG="$(basename "$0")"
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]"
echo
echo " Options are:"
echo " -O official release (not release-candidate)"
echo " -j INT maximum number of parallel jobs (default 1)"
echo " -l build library"
echo " -r RELEASE proper release with name"
echo
echo " Make Isabelle distribution DIR, using the local repository clone."
echo
echo " VERSION identifies the snapshot, using usual Mercurial terminology;"
echo " the default is RELEASE if given, otherwise \"tip\"."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
function check_number()
{
[ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
}
## process command line
# options
OFFICIAL_RELEASE=""
JOBS=""
LIBRARY=""
RELEASE=""
while getopts "Oj:lr:" OPT
do
case "$OPT" in
O)
OFFICIAL_RELEASE="-O"
;;
j)
check_number "$OPTARG"
JOBS="-j $OPTARG"
;;
l)
LIBRARY="true"
;;
r)
RELEASE="$OPTARG"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
BASE_DIR=""
[ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; }
[ -z "$BASE_DIR" ] && usage
VERSION=""
[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
[ -z "$VERSION" ] && VERSION="$RELEASE"
[ -z "$VERSION" ] && VERSION="tip"
[ "$#" -gt 0 ] && usage
## Isabelle settings
ISABELLE_TOOL="$THIS/../../bin/isabelle"
ISABELLE_PLATFORM_FAMILY="$("$ISABELLE_TOOL" getenv -b ISABELLE_PLATFORM_FAMILY)"
## main
# make dist
if [ -z "$RELEASE" ]; then
DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")"
"$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE
else
DISTNAME="$RELEASE"
"$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE -r "$RELEASE"
fi
[ "$?" = 0 ] || exit "$?"
DISTBASE="$BASE_DIR/dist-${DISTNAME}"
# make bundles
for PLATFORM_FAMILY in linux macos windows
do
echo
echo "*** $PLATFORM_FAMILY ***"
"$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$PLATFORM_FAMILY"
[ "$?" = 0 ] || exit "$?"
done
# minimal index
cat > "$DISTBASE/index.html" <<EOF
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
<html>
<head>
<title>${DISTNAME}</title>
</head>
<body>
<h1>${DISTNAME}</h1>
<ul>
<li><a href="${DISTNAME}_linux.tar.gz">Linux</a></li>
<li><a href="${DISTNAME}.exe">Windows</a></li>
<li><a href="${DISTNAME}.dmg">Mac OS X</a></li>
</ul>
</body>
</html>
EOF
# HTML library
if [ -n "$LIBRARY" ]; then
"$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
fi