lib/Tools/setup
author wenzelm
Sat, 27 Mar 2021 20:53:11 +0100
changeset 73745 d31d229eb8df
parent 73744 9460f1f45405
child 73746 dbe5bbc2331e
permissions -rwxr-xr-x
more robust;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73742
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"
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    19
  echo "    -C           enforce clean update of working directory (no backup!)"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    20
  echo "    -V PATH      version from explicit file or directory (file \"ISABELLE_VERSION\")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    21
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    22
  echo "  Setup the current ISABELLE_HOME directory, which needs to be a"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    23
  echo "  repository clone (all versions) or repository archive (fixed version)."
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    24
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    25
  exit 1
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    26
}
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    27
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    28
function fail()
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    29
{
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    30
  echo "$1" >&2
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    31
  exit 2
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
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    35
## process command line
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    36
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    37
#options
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    38
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    39
CLEAN=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    40
VERSION_PATH=""
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    41
VERSION_REV=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    42
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    43
while getopts "CV:r:" OPT
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    44
do
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    45
  case "$OPT" in
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    46
    C)
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    47
      CLEAN="--clean"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    48
      ;;
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    49
    V)
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    50
      VERSION_PATH="$OPTARG"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    51
      ;;
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    52
    r)
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    53
      VERSION_REV="$OPTARG"
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    54
      ;;
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    55
    \?)
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    56
      usage
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    57
      ;;
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    58
  esac
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    59
done
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    60
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    61
shift $(($OPTIND - 1))
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
# args
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    65
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    66
[ "$#" -ne 0 ] && usage
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    67
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    68
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    69
## main
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    70
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    71
if [ -z "$VERSION_REV" -a -z "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    72
  isabelle components -I && isabelle components -a
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    73
elif [ -n "$VERSION_REV" -a -n "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    74
  fail "Duplicate version specification (options -r and -V)"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    75
elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    76
  fail "Not a repository clone: cannot specify version"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    77
else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    78
  export REV=""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    79
  if [ -n "$VERSION_REV" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    80
    REV="$VERSION_REV"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    81
  elif [ -f "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    82
    REV="$(cat "$VERSION_PATH")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    83
  elif [ -d "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    84
    if [ -f "$VERSION_PATH/ISABELLE_VERSION" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    85
      REV="$(cat "$VERSION_PATH/ISABELLE_VERSION")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    86
    else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    87
      fail "Missing file \"$VERSION_PATH/ISABELLE_VERSION\""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    88
    fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    89
  else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    90
    fail "Missing file \"$VERSION_PATH\""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    91
  fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    92
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    93
  export LANG=C
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    94
  export HGPLAIN=
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    95
73744
9460f1f45405 more robust: explicit repository root;
wenzelm
parents: 73743
diff changeset
    96
  if "${HG:-hg}" -R "$ISABELLE_HOME" id -r "$REV" >/dev/null 2>/dev/null
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    97
  then
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    98
    PULL=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    99
  else
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
   100
    PULL=true
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   101
  fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   102
73745
d31d229eb8df more robust;
wenzelm
parents: 73744
diff changeset
   103
  isabelle components -I || exit "$?"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   104
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   105
  #Atomic exec: avoid inplace update of running script!
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
   106
  export CLEAN PULL
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   107
  exec bash -c '
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   108
    set -e
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   109
    if [ -n "$PULL" ]; then
73744
9460f1f45405 more robust: explicit repository root;
wenzelm
parents: 73743
diff changeset
   110
      "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   111
    fi
73744
9460f1f45405 more robust: explicit repository root;
wenzelm
parents: 73743
diff changeset
   112
    "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
   113
    isabelle components -a
73744
9460f1f45405 more robust: explicit repository root;
wenzelm
parents: 73743
diff changeset
   114
    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   115
  '
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   116
fi