lib/Tools/components
author wenzelm
Thu, 21 Jan 2021 16:10:43 +0100
changeset 73172 fc828f64da5b
parent 72524 8e9312e6a6d9
child 73308 f73c691bd679
permissions -rwxr-xr-x
support isabelle components -u and -x;
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"
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    22
  echo "    -u DIR       update \$ISABELLE_HOME_USER/components: add directory"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    23
  echo "    -x DIR       update \$ISABELLE_HOME_USER/components: remove directory"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    24
  echo
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    25
  echo "  Resolve Isabelle components via download and installation: given COMPONENTS"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    26
  echo "  are identified via base name. Further operations manage etc/settings and"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
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\""
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
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=""
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    50
declare -a UPDATE_COMPONENTS=()
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    51
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
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
      ;;
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    67
    u)
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    68
      UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="+$OPTARG"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    69
      ;;
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    70
    x)
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
    71
      UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="-$OPTARG"
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
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
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
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"
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69379
diff changeset
   101
  SETTINGS_CONTENT='init_components "$ISABELLE_COMPONENTS_BASE" "$ISABELLE_HOME/Admin/components/main"'
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   102
  if [ -e "$SETTINGS" ]; then
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   103
    echo "User settings file already exists!"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   104
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   105
    echo "Edit \"$SETTINGS\" manually"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   106
    echo "and add the following line near its start:"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   107
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   108
    echo "  $SETTINGS_CONTENT"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   109
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   110
  else
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   111
    echo "Initializing \"$SETTINGS\""
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   112
    mkdir -p "$(dirname "$SETTINGS")"
72524
8e9312e6a6d9 clarified generated settings;
wenzelm
parents: 72409
diff changeset
   113
    {
8e9312e6a6d9 clarified generated settings;
wenzelm
parents: 72409
diff changeset
   114
      echo "#-*- shell-script -*- :mode=shellscript:"
8e9312e6a6d9 clarified generated settings;
wenzelm
parents: 72409
diff changeset
   115
      echo
8e9312e6a6d9 clarified generated settings;
wenzelm
parents: 72409
diff changeset
   116
      echo "$SETTINGS_CONTENT"
8e9312e6a6d9 clarified generated settings;
wenzelm
parents: 72409
diff changeset
   117
    } > "$SETTINGS"
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   118
  fi
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   119
elif [ -n "$LIST_ONLY" ]; then
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   120
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   121
  echo "Available components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   122
  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   123
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   124
  echo "Missing components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   125
  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
   126
elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
   127
  isabelle_admin_build jars || exit $?
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 72524
diff changeset
   128
  exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   129
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   130
  for NAME in "${SELECTED_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   131
  do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   132
    BASE_NAME="$(basename "$NAME")"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   133
    FULL_NAME=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   134
    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   135
    do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   136
      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   137
    done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   138
    if [ -z "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   139
      echo "Ignoring irrelevant component \"$NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   140
    elif [ -d "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   141
      echo "Skipping existing component \"$FULL_NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   142
    else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   143
      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   144
        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
63490
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 53435
diff changeset
   145
        type -p curl > /dev/null || fail "Cannot download files: missing curl"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   146
        echo "Getting \"$REMOTE\""
48841
90fe0798b83a minor robustification;
wenzelm
parents: 48840
diff changeset
   147
        mkdir -p "$(dirname "$FULL_NAME")"
72409
da577e2d42b3 clarified according to Isabelle_System.download;
wenzelm
parents: 69434
diff changeset
   148
        curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \
63490
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 53435
diff changeset
   149
          fail "Failed to download \"$REMOTE\""
69379
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   150
        if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   151
        then
69379
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   152
          rm -f "${FULL_NAME}.tar.gz.part"
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   153
        else
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   154
          mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   155
        fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   156
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   157
      if [ -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   158
        echo "Unpacking \"${FULL_NAME}.tar.gz\""
53314
be1c07ec768f check tar error, e.g. from corrupted download;
wenzelm
parents: 50653
diff changeset
   159
        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   160
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   161
    fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   162
  done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   163
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   164