diff --git a/lib/Tools/setup b/lib/Tools/setup --- a/lib/Tools/setup +++ b/lib/Tools/setup @@ -1,116 +1,140 @@ #!/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 " -r REV explicit Mercurial version" + echo " -r REV version according to Mercurial notation" 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 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 "CV:r:" OPT +while getopts "CRU:V:r:" 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" ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -ne 0 ] && usage ## main -if [ -z "$VERSION_REV" -a -z "$VERSION_PATH" ]; then +if [ -z "$VERSION" ]; then isabelle components -I && isabelle components -a -elif [ -n "$VERSION_REV" -a -n "$VERSION_PATH" ]; then - fail "Duplicate version specification (options -r and -V)" elif [ ! -d "$ISABELLE_HOME/.hg" ]; then fail "Not a repository clone: cannot specify version" else export REV="" 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= if "${HG:-hg}" -R "$ISABELLE_HOME" id -r "$REV" >/dev/null 2>/dev/null then PULL="" else PULL=true fi isabelle components -I || exit "$?" #Atomic exec: avoid inplace update of running script! export CLEAN PULL exec bash -c ' set -e if [ -n "$PULL" ]; then - "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" + "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS" fi "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN isabelle components -a "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV" ' fi