Admin/setup
author wenzelm
Sun, 28 Mar 2021 12:02:20 +0200
changeset 73760 a35b2ee3148f
parent 73759 c259c7a42ac3
child 73761 d34033a93711
permissions -rwxr-xr-x
proper export;
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
73756
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
     8
## environment
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
     9
73756
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
    10
export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
73742
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
73756
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
    14
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
    15
## diagnostics
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
    16
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    17
function usage()
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    18
{
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    19
  echo
73756
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
    20
  echo "Usage: Admin/setup [OPTIONS]"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    21
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    22
  echo "  Options are:"
73757
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
    23
  echo "    -C           force clean working directory (no backup!)"
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    24
  echo "    -R           version is current official release"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    25
  echo "    -U URL       Isabelle repository server (default: \"$ISABELLE_REPOS\")"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    26
  echo "    -V PATH      version from explicit file or directory (file \"ISABELLE_VERSION\")"
73757
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
    27
  echo "    -c           check clean working directory"
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    28
  echo "    -f           fresh build of Isabelle/Scala/jEdit"
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    29
  echo "    -n           no build of Isabelle/Scala/jEdit"
73748
827f53095f1c more robust: lest hg work out remote tip;
wenzelm
parents: 73747
diff changeset
    30
  echo "    -r REV       version according to Mercurial notation"
73747
8c93418ea257 more options;
wenzelm
parents: 73746
diff changeset
    31
  echo "    -u           version is remote tip"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    32
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    33
  echo "  Setup the current ISABELLE_HOME directory, which needs to be a"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    34
  echo "  repository clone (all versions) or repository archive (fixed version)."
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    35
  echo
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    36
  exit 1
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
function fail()
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    40
{
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    41
  echo "$1" >&2
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    42
  exit 2
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    43
}
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    44
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    45
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    46
## process command line
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    47
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    48
#options
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    49
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    50
BUILD_OPTIONS="-b"
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    51
73757
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
    52
CLEAN_FORCE=""
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
    53
CLEAN_CHECK=""
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    54
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    55
VERSION=""
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    56
VERSION_RELEASE=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    57
VERSION_PATH=""
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    58
VERSION_REV=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    59
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    60
while getopts "CRU:V:cfnr:u" OPT
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    61
do
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    62
  case "$OPT" in
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    63
    C)
73757
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
    64
      CLEAN_FORCE="--clean"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    65
      ;;
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    66
    R)
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="true"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    69
      VERSION_PATH=""
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    70
      VERSION_REV=""
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    71
      ;;
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    72
    U)
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    73
      ISABELLE_REPOS="$OPTARG"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    74
      ;;
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    75
    V)
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    76
      VERSION="true"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    77
      VERSION_RELEASE=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    78
      VERSION_PATH="$OPTARG"
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    79
      VERSION_REV=""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
    80
      ;;
73757
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
    81
    c)
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
    82
      CLEAN_CHECK="--check"
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
    83
      ;;
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    84
    f)
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    85
      BUILD_OPTIONS="-b -f"
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    86
      ;;
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    87
    n)
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    88
      BUILD_OPTIONS=""
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
    89
      ;;
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    90
    r)
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    91
      VERSION="true"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    92
      VERSION_RELEASE=""
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
    93
      VERSION_PATH=""
73743
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    94
      VERSION_REV="$OPTARG"
97692af929a4 more robust;
wenzelm
parents: 73742
diff changeset
    95
      ;;
73747
8c93418ea257 more options;
wenzelm
parents: 73746
diff changeset
    96
    u)
8c93418ea257 more options;
wenzelm
parents: 73746
diff changeset
    97
      VERSION="true"
8c93418ea257 more options;
wenzelm
parents: 73746
diff changeset
    98
      VERSION_RELEASE=""
8c93418ea257 more options;
wenzelm
parents: 73746
diff changeset
    99
      VERSION_PATH=""
73748
827f53095f1c more robust: lest hg work out remote tip;
wenzelm
parents: 73747
diff changeset
   100
      VERSION_REV="tip"
73747
8c93418ea257 more options;
wenzelm
parents: 73746
diff changeset
   101
      ;;
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   102
    \?)
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   103
      usage
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   104
      ;;
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   105
  esac
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   106
done
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   107
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   108
shift $(($OPTIND - 1))
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   109
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   110
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   111
# args
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   112
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   113
[ "$#" -ne 0 ] && usage
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   114
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   115
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   116
## main
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   117
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   118
if [ -z "$VERSION" ]; then
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
   119
  "$ISABELLE_HOME/bin/isabelle" components -I || exit "?$"
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
   120
  "$ISABELLE_HOME/bin/isabelle" components -a || exit "?$"
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
   121
  if [ -n "$BUILD_OPTIONS" ]; then
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
   122
    "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
   123
  fi
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   124
elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   125
  fail "Not a repository clone: cannot specify version"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   126
else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   127
  if [ -n "$VERSION_REV" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   128
    REV="$VERSION_REV"
73746
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   129
  elif [ -n "$VERSION_RELEASE" ]; then
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   130
    URL="$ISABELLE_REPOS/raw-file/tip/Admin/Release/official"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   131
    REV="$(curl -s -f "$URL" | head -n1)"
dbe5bbc2331e clarified treatment of multiple versions: last one counts;
wenzelm
parents: 73745
diff changeset
   132
    [ -z "$REV" ] && fail "Failed to access \"$URL\""
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   133
  elif [ -f "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   134
    REV="$(cat "$VERSION_PATH")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   135
  elif [ -d "$VERSION_PATH" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   136
    if [ -f "$VERSION_PATH/ISABELLE_VERSION" ]; then
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   137
      REV="$(cat "$VERSION_PATH/ISABELLE_VERSION")"
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   138
    else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   139
      fail "Missing file \"$VERSION_PATH/ISABELLE_VERSION\""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   140
    fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   141
  else
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   142
    fail "Missing file \"$VERSION_PATH\""
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   143
  fi
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   144
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   145
  export LANG=C
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   146
  export HGPLAIN=
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   147
73756
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
   148
  "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   149
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   150
  #Atomic exec: avoid inplace update of running script!
73760
a35b2ee3148f proper export;
wenzelm
parents: 73759
diff changeset
   151
  export CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   152
  exec bash -c '
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   153
    set -e
73748
827f53095f1c more robust: lest hg work out remote tip;
wenzelm
parents: 73747
diff changeset
   154
    "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
73757
c582bf975a5b more options;
wenzelm
parents: 73756
diff changeset
   155
    "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN_FORCE $CLEAN_CHECK
73756
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
   156
    "$ISABELLE_HOME/bin/isabelle" components -a
73759
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
   157
    if [ -n "$BUILD_OPTIONS" ]; then
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
   158
      "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
c259c7a42ac3 more options: build is part of default setup;
wenzelm
parents: 73757
diff changeset
   159
    fi
73744
9460f1f45405 more robust: explicit repository root;
wenzelm
parents: 73743
diff changeset
   160
    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
73756
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
   161
    if [ ! -f "$ISABELLE_HOME/Admin/setup" ]; then
f026a9a0a43f proper Admin script, outside the settings environment;
wenzelm
parents: 73752
diff changeset
   162
      echo >&2 "### The Admin/setup script has disappeared in this version"
73752
7cdcf131699d tuned message;
wenzelm
parents: 73751
diff changeset
   163
      echo >&2 "### (need to invoke \"${HG:-hg} update\" before using it again)"
73749
e16133a05458 clarified messages;
wenzelm
parents: 73748
diff changeset
   164
    fi
73742
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   165
  '
47f055b40ab9 more convenient repository setup;
wenzelm
parents:
diff changeset
   166
fi