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