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