#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: setup for Isabelle repository clone or repository archive
## diagnostics
PRG="$(basename "$0")"
ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS]"
echo
echo " Options are:"
echo " -C enforce clean update of working directory (no backup!)"
echo " -R version is current official release"
echo " -U URL Isabelle repository server (default: \"$ISABELLE_REPOS\")"
echo " -V PATH version from explicit file or directory (file \"ISABELLE_VERSION\")"
echo " -r REV version according to Mercurial notation"
echo " -u version is remote tip"
echo
echo " Setup the current ISABELLE_HOME directory, which needs to be a"
echo " repository clone (all versions) or repository archive (fixed version)."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
#options
CLEAN=""
VERSION=""
VERSION_RELEASE=""
VERSION_PATH=""
VERSION_REV=""
while getopts "CRU:V:r:u" OPT
do
case "$OPT" in
C)
CLEAN="--clean"
;;
R)
VERSION="true"
VERSION_RELEASE="true"
VERSION_PATH=""
VERSION_REV=""
;;
U)
ISABELLE_REPOS="$OPTARG"
;;
V)
VERSION="true"
VERSION_RELEASE=""
VERSION_PATH="$OPTARG"
VERSION_REV=""
;;
r)
VERSION="true"
VERSION_RELEASE=""
VERSION_PATH=""
VERSION_REV="$OPTARG"
;;
u)
VERSION="true"
VERSION_RELEASE=""
VERSION_PATH=""
VERSION_REV="tip"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
[ "$#" -ne 0 ] && usage
## main
if [ -z "$VERSION" ]; then
isabelle components -I && isabelle components -a
elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
fail "Not a repository clone: cannot specify version"
else
if [ -n "$VERSION_REV" ]; then
REV="$VERSION_REV"
elif [ -n "$VERSION_RELEASE" ]; then
URL="$ISABELLE_REPOS/raw-file/tip/Admin/Release/official"
REV="$(curl -s -f "$URL" | head -n1)"
[ -z "$REV" ] && fail "Failed to access \"$URL\""
elif [ -f "$VERSION_PATH" ]; then
REV="$(cat "$VERSION_PATH")"
elif [ -d "$VERSION_PATH" ]; then
if [ -f "$VERSION_PATH/ISABELLE_VERSION" ]; then
REV="$(cat "$VERSION_PATH/ISABELLE_VERSION")"
else
fail "Missing file \"$VERSION_PATH/ISABELLE_VERSION\""
fi
else
fail "Missing file \"$VERSION_PATH\""
fi
export LANG=C
export HGPLAIN=
isabelle components -I || exit "$?"
#Atomic exec: avoid inplace update of running script!
export CLEAN REV ISABELLE_REPOS
exec bash -c '
set -e
"${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
"${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN
isabelle components -a
"${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
'
fi