lib/Tools/setup
author wenzelm
Sat, 27 Mar 2021 21:27:27 +0100
changeset 73746 dbe5bbc2331e
parent 73745 d31d229eb8df
child 73747 8c93418ea257
permissions -rwxr-xr-x
clarified treatment of multiple versions: last one counts; more options;
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
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    12
ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    13
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    14
function usage()
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    15
{
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    16
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    17
  echo "Usage: isabelle $PRG [OPTIONS]"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    18
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    19
  echo "  Options are:"
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    20
  echo "    -r REV       version according to Mercurial notation"
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    21
  echo "    -C           enforce clean update of working directory (no backup!)"
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    22
  echo "    -R           version is current official release"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    23
  echo "    -U URL       Isabelle repository server (default: \"$ISABELLE_REPOS\")"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    24
  echo "    -V PATH      version from explicit file or directory (file \"ISABELLE_VERSION\")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    25
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    26
  echo "  Setup the current ISABELLE_HOME directory, which needs to be a"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    27
  echo "  repository clone (all versions) or repository archive (fixed version)."
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    28
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    29
  exit 1
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    30
}
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    31
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    32
function fail()
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    33
{
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    34
  echo "$1" >&2
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    35
  exit 2
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    36
}
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    37
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    38
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    39
## process command line
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    40
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    41
#options
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    42
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    43
CLEAN=""
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    44
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    45
VERSION=""
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    46
VERSION_RELEASE=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    47
VERSION_PATH=""
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    48
VERSION_REV=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    49
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    50
while getopts "CRU:V:r:" OPT
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    51
do
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    52
  case "$OPT" in
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    53
    C)
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    54
      CLEAN="--clean"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    55
      ;;
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    56
    R)
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    57
      VERSION="true"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    58
      VERSION_RELEASE="true"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    59
      VERSION_PATH=""
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    60
      VERSION_REV=""
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    61
      ;;
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    62
    U)
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    63
      ISABELLE_REPOS="$OPTARG"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    64
      ;;
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    65
    V)
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    66
      VERSION="true"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    67
      VERSION_RELEASE=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    68
      VERSION_PATH="$OPTARG"
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    69
      VERSION_REV=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    70
      ;;
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    71
    r)
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    72
      VERSION="true"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    73
      VERSION_RELEASE=""
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    74
      VERSION_PATH=""
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    75
      VERSION_REV="$OPTARG"
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    76
      ;;
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    77
    \?)
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    78
      usage
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    79
      ;;
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    80
  esac
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    81
done
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    82
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    83
shift $(($OPTIND - 1))
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    84
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    85
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    86
# args
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    87
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    88
[ "$#" -ne 0 ] && usage
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    89
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    90
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    91
## main
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    92
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    93
if [ -z "$VERSION" ]; then
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    94
  isabelle components -I && isabelle components -a
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    95
elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    96
  fail "Not a repository clone: cannot specify version"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    97
else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    98
  export REV=""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    99
  if [ -n "$VERSION_REV" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   100
    REV="$VERSION_REV"
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   101
  elif [ -n "$VERSION_RELEASE" ]; then
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   102
    URL="$ISABELLE_REPOS/raw-file/tip/Admin/Release/official"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   103
    REV="$(curl -s -f "$URL" | head -n1)"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   104
    [ -z "$REV" ] && fail "Failed to access \"$URL\""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   105
  elif [ -f "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   106
    REV="$(cat "$VERSION_PATH")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   107
  elif [ -d "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   108
    if [ -f "$VERSION_PATH/ISABELLE_VERSION" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   109
      REV="$(cat "$VERSION_PATH/ISABELLE_VERSION")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   110
    else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   111
      fail "Missing file \"$VERSION_PATH/ISABELLE_VERSION\""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   112
    fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   113
  else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   114
    fail "Missing file \"$VERSION_PATH\""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   115
  fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   116
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   117
  export LANG=C
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   118
  export HGPLAIN=
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   119
73744
9460f1f45405 more robust: explicit repository root;
wenzelm
parents: 73743
diff changeset
   120
  if "${HG:-hg}" -R "$ISABELLE_HOME" id -r "$REV" >/dev/null 2>/dev/null
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   121
  then
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
   122
    PULL=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   123
  else
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
   124
    PULL=true
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   125
  fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   126
73745
d31d229eb8df more robust;
wenzelm
parents: 73744
diff changeset
   127
  isabelle components -I || exit "$?"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   128
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   129
  #Atomic exec: avoid inplace update of running script!
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
   130
  export CLEAN PULL
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   131
  exec bash -c '
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   132
    set -e
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   133
    if [ -n "$PULL" ]; then
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   134
      "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   135
    fi
73744
9460f1f45405 more robust: explicit repository root;
wenzelm
parents: 73743
diff changeset
   136
    "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
   137
    isabelle components -a
73744
9460f1f45405 more robust: explicit repository root;
wenzelm
parents: 73743
diff changeset
   138
    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   139
  '
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   140
fi