lib/Tools/components
author wenzelm
Wed, 31 Mar 2021 11:24:46 +0200
changeset 73772 d3f2038198ae
parent 73739 4f8849357ba7
child 74281 b4e6b82fdb9e
permissions -rwxr-xr-x
clarified (again): local tip could be actually more recent;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     2
#
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     4
#
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: resolve Isabelle components
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     6
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     7
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     8
## diagnostics
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     9
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    11
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    12
function usage()
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    13
{
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    14
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    16
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    18
  echo "    -I           init user settings"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    19
  echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
53435
wenzelm
parents: 53314
diff changeset
    20
  echo "    -a           resolve all missing components"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    21
  echo "    -l           list status"
73555
f73c691bd679 clarified message;
wenzelm
parents: 73417
diff changeset
    22
  echo "    -u DIR       update \$ISABELLE_HOME_USER/etc/components: add directory"
f73c691bd679 clarified message;
wenzelm
parents: 73417
diff changeset
    23
  echo "    -x DIR       update \$ISABELLE_HOME_USER/etc/components: remove directory"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    24
  echo
73417
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    25
  echo "  Resolve Isabelle components via download and installation: given COMPONENTS"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    26
  echo "  are identified via base name. Further operations manage etc/settings and"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    27
  echo "  etc/components in \$ISABELLE_HOME_USER."
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    28
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    29
  echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
73417
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    30
  echo "  ISABELLE_HOME_USER=\"$ISABELLE_HOME_USER\""
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    31
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    32
  exit 1
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    33
}
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    34
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    35
function fail()
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    36
{
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    37
  echo "$1" >&2
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    38
  exit 2
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    39
}
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    40
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    41
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    42
## process command line
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    43
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    44
#options
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    45
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    46
INIT_SETTINGS=""
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    47
COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    48
ALL_MISSING=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    49
LIST_ONLY=""
73417
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    50
declare -a UPDATE_COMPONENTS=()
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    51
73417
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    52
while getopts "IR:alu:x:" OPT
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    53
do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    54
  case "$OPT" in
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    55
    I)
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    56
      INIT_SETTINGS="true"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    57
      ;;
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    58
    R)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    59
      COMPONENT_REPOSITORY="$OPTARG"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    60
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    61
    a)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    62
      ALL_MISSING="true"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    63
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    64
    l)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    65
      LIST_ONLY="true"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    66
      ;;
73417
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    67
    u)
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    68
      UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="+$OPTARG"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    69
      ;;
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    70
    x)
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    71
      UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="-$OPTARG"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    72
      ;;
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    73
    \?)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    74
      usage
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    75
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    76
  esac
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    77
done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    78
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    79
shift $(($OPTIND - 1))
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    80
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    81
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    82
# args
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    83
73417
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
    84
[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" -a "${#UPDATE_COMPONENTS[@]}" -eq 0 ] && usage
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    85
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    86
if [ -z "$ALL_MISSING" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    87
  splitarray ":" "$@"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    88
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    89
  splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    90
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    91
declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    92
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    93
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    94
## main
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    95
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    96
splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    97
splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    98
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    99
if [ -n "$INIT_SETTINGS" ]; then
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   100
  SETTINGS="$ISABELLE_HOME_USER/etc/settings"
73739
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   101
  SETTINGS_CONTENT='init_components "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" "$ISABELLE_HOME/Admin/components/main"'
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   102
  if [ ! -e "$SETTINGS" ]; then
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   103
    echo "Initializing \"$SETTINGS\""
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   104
    mkdir -p "$(dirname "$SETTINGS")"
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   105
    {
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   106
      echo "#-*- shell-script -*- :mode=shellscript:"
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   107
      echo
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   108
      echo "$SETTINGS_CONTENT"
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   109
    } > "$SETTINGS"
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   110
  elif grep "init_components.*components/main" "$SETTINGS" >/dev/null 2>/dev/null
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   111
  then
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   112
    :
4f8849357ba7 more robust: idempotent;
wenzelm
parents: 73654
diff changeset
   113
  else
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   114
    echo "User settings file already exists!"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   115
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   116
    echo "Edit \"$SETTINGS\" manually"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   117
    echo "and add the following line near its start:"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   118
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   119
    echo "  $SETTINGS_CONTENT"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   120
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   121
  fi
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   122
elif [ -n "$LIST_ONLY" ]; then
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   123
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   124
  echo "Available components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   125
  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   126
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   127
  echo "Missing components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   128
  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
73417
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
   129
elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
   130
  isabelle_admin_build jars || exit $?
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72762
diff changeset
   131
  exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   132
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   133
  for NAME in "${SELECTED_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   134
  do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   135
    BASE_NAME="$(basename "$NAME")"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   136
    FULL_NAME=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   137
    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   138
    do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   139
      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   140
    done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   141
    if [ -z "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   142
      echo "Ignoring irrelevant component \"$NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   143
    elif [ -d "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   144
      echo "Skipping existing component \"$FULL_NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   145
    else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   146
      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   147
        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
63490
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 53435
diff changeset
   148
        type -p curl > /dev/null || fail "Cannot download files: missing curl"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   149
        echo "Getting \"$REMOTE\""
48841
90fe0798b83a minor robustification;
wenzelm
parents: 48840
diff changeset
   150
        mkdir -p "$(dirname "$FULL_NAME")"
73654
7eecb5231f61 more robust;
wenzelm
parents: 73555
diff changeset
   151
        if curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   152
        then
73654
7eecb5231f61 more robust;
wenzelm
parents: 73555
diff changeset
   153
          mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
69389
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   154
        else
73654
7eecb5231f61 more robust;
wenzelm
parents: 73555
diff changeset
   155
          rm -f "${FULL_NAME}.tar.gz.part"
7eecb5231f61 more robust;
wenzelm
parents: 73555
diff changeset
   156
          fail "Failed to download \"$REMOTE\""
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   157
        fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   158
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   159
      if [ -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   160
        echo "Unpacking \"${FULL_NAME}.tar.gz\""
53314
be1c07ec768f check tar error, e.g. from corrupted download;
wenzelm
parents: 50653
diff changeset
   161
        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   162
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   163
    fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   164
  done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   165
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   166