lib/Tools/setup

more robust: explicit repository root;

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: setup for Isabelle repository clone or repository archive


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -r REV       explicit Mercurial version"
  echo "    -C           enforce clean update of working directory (no backup!)"
  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_PATH=""
VERSION_REV=""

while getopts "CV:r:" OPT
do
  case "$OPT" in
    C)
      CLEAN="--clean"
      ;;
    V)
      VERSION_PATH="$OPTARG"
      ;;
    r)
      VERSION_REV="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 ] && usage


## main

if [ -z "$VERSION_REV" -a -z "$VERSION_PATH" ]; 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 [ -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

  #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"
    fi
    "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN
    isabelle components -a
    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
  '
fi