lib/Tools/setup
author wenzelm
Sat, 27 Mar 2021 20:24:04 +0100
changeset 73487 47f055b40ab9
child 73488 97692af929a4
permissions -rwxr-xr-x
more convenient repository setup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73487
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     2
#
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     4
#
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: setup for Isabelle repository clone or repository archive
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     6
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     7
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     8
## diagnostics
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     9
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    11
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    12
function usage()
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    13
{
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    14
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS]"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    16
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    18
  echo "    -r REV       explicit Mercurial version"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    19
  echo "    -V PATH      version from explicit file or directory (file \"ISABELLE_VERSION\")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    20
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    21
  echo "  Setup the current ISABELLE_HOME directory, which needs to be a"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    22
  echo "  repository clone (all versions) or repository archive (fixed version)."
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    23
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    24
  exit 1
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    25
}
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    26
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    27
function fail()
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    28
{
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    29
  echo "$1" >&2
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    30
  exit 2
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    31
}
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    32
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    33
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    34
## process command line
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    35
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    36
#options
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    37
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    38
VERSION_REV=""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    39
VERSION_PATH=""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    40
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    41
while getopts "r:V:" OPT
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    42
do
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    43
  case "$OPT" in
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    44
    r)
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    45
      VERSION_REV="$OPTARG"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    46
      ;;
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    47
    V)
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    48
      VERSION_PATH="$OPTARG"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    49
      ;;
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    50
    \?)
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    51
      usage
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    52
      ;;
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    53
  esac
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    54
done
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    55
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    56
shift $(($OPTIND - 1))
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    57
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    58
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    59
# args
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    60
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    61
[ "$#" -ne 0 ] && usage
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    62
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    63
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    64
## main
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    65
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    66
if [ -z "$VERSION_REV" -a -z "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    67
  isabelle components -I && isabelle components -a
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    68
elif [ -n "$VERSION_REV" -a -n "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    69
  fail "Duplicate version specification (options -r and -V)"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    70
elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    71
  fail "Not a repository clone: cannot specify version"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    72
else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    73
  export REV=""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    74
  if [ -n "$VERSION_REV" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    75
    REV="$VERSION_REV"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    76
  elif [ -f "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    77
    REV="$(cat "$VERSION_PATH")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    78
  elif [ -d "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    79
    if [ -f "$VERSION_PATH/ISABELLE_VERSION" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    80
      REV="$(cat "$VERSION_PATH/ISABELLE_VERSION")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    81
    else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    82
      fail "Missing file \"$VERSION_PATH/ISABELLE_VERSION\""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    83
    fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    84
  else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    85
    fail "Missing file \"$VERSION_PATH\""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    86
  fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    87
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    88
  export LANG=C
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    89
  export HGPLAIN=
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    90
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    91
  if "${HG:-hg}" id -r "$REV" >/dev/null 2>/dev/null
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    92
  then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    93
    export PULL=""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    94
  else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    95
    export PULL=true
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    96
  fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    97
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    98
  isabelle components -I
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    99
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   100
  #Atomic exec: avoid inplace update of running script!
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   101
  exec bash -c '
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   102
    set -e
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   103
    if [ -n "$PULL" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   104
      "${HG:-hg}" pull -r "$REV"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   105
    fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   106
    "${HG:-hg}" update -r "$REV"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   107
    "${HG:-hg}" log -r "$REV"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   108
    isabelle components -a
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   109
  '
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   110
fi