Admin/init

replaced some lemmas' implicit formulas by explicit ones to avoid silent changes

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


## environment

unset CDPATH
export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"

ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle"


## diagnostics

function usage()
{
  echo
  echo "Usage: Admin/init [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -C           force clean working directory (no backup!)"
  echo "    -I NAME      set \$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER (or reset via -I:)"
  echo "    -L           local history only: no pull from repository server"
  echo "    -R           version is current official release"
  echo "    -U URL       Isabelle repository server"
  echo "                 (default: \"$ISABELLE_REPOS\")"
  echo "    -V PATH      version is taken from file, or directory"
  echo "                 with file \"ISABELLE_VERSION\""
  echo "    -c           check clean working directory"
  echo "    -f           fresh build of Isabelle/Scala/jEdit"
  echo "    -n           no build of Isabelle/Scala/jEdit"
  echo "    -r REV       version given in Mercurial notation (changeset id or tag)"
  echo "    -u           update to latest tip"
  echo
  echo "  Initialize the current ISABELLE_HOME directory, which needs to be a"
  echo "  repository clone (all versions) or repository archive (fixed version)."
  echo "  Download required components. Build Isabelle/Scala/jEdit by default."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

#options

BUILD_OPTIONS="-b"
UPDATE_IDENTIFIER=""
IDENTIFIER=""
PULL="true"

CLEAN_FORCE=""
CLEAN_CHECK=""

VERSION=""
VERSION_RELEASE=""
VERSION_PATH=""
VERSION_REV=""

while getopts "CI:LRU:V:cfnr:u" OPT
do
  case "$OPT" in
    C)
      CLEAN_FORCE="--clean"
      ;;
    I)
      UPDATE_IDENTIFIER="true"
      if [ "$OPTARG" = ":" ]; then
        IDENTIFIER=""
      else
        IDENTIFIER="$OPTARG"
      fi
      ;;
    L)
      PULL=""
      ;;
    R)
      VERSION="true"
      VERSION_RELEASE="true"
      VERSION_PATH=""
      VERSION_REV=""
      ;;
    U)
      ISABELLE_REPOS="$OPTARG"
      ;;
    V)
      VERSION="true"
      VERSION_RELEASE=""
      VERSION_PATH="$OPTARG"
      VERSION_REV=""
      ;;
    c)
      CLEAN_CHECK="--check"
      ;;
    f)
      BUILD_OPTIONS="-b -f"
      ;;
    n)
      BUILD_OPTIONS=""
      ;;
    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 [ -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER" ]; then
  OLD_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")"
else
  OLD_IDENTIFIER=""
fi

if [ -n "$UPDATE_IDENTIFIER" -a "$IDENTIFIER" != "$OLD_IDENTIFIER" ]; then
  OLD_ISABELLE_HOME_USER="$("$ISABELLE_HOME/bin/isabelle" getenv -b ISABELLE_HOME_USER)"
  if [ -n "$IDENTIFIER" ]; then
    echo -n "$IDENTIFIER" > "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER"
  else
    rm -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER"
  fi
  ISABELLE_HOME_USER="$("$ISABELLE_HOME/bin/isabelle" getenv -b ISABELLE_HOME_USER)"
  echo "Changed \$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER: \"$OLD_IDENTIFIER\" ~> \"$IDENTIFIER\""
  echo "Changed \$ISABELLE_HOME_USER: \"$OLD_ISABELLE_HOME_USER\" ~> \"$ISABELLE_HOME_USER\""
fi

if [ -z "$VERSION" ]; then
  "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
  "$ISABELLE_HOME/bin/isabelle" components -a || exit "$?"
  if [ -n "$BUILD_OPTIONS" ]; then
    "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
  fi
elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
  fail "Not a repository clone: cannot switch 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

  "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"

  export LANG=C
  export HGPLAIN=

  #Atomic exec: avoid inplace update of running script!
  export PULL CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
  exec bash -c '
    set -e
    if [ -n "$PULL" ]; then
      "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
    fi
    "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN_FORCE $CLEAN_CHECK
    "$ISABELLE_HOME/bin/isabelle" components -a
    if [ -n "$BUILD_OPTIONS" ]; then
      "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
    fi
    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
    if [ ! -f "$ISABELLE_HOME/Admin/init" ]; then
      echo >&2 "### The Admin/init script has disappeared in this version"
      echo >&2 "### (need to invoke \"${HG:-hg} update\" before using it again)"
    fi
  '
fi