lib/Tools/components
author wenzelm
Tue, 05 Nov 2019 14:28:00 +0100
changeset 71047 87c132cf5860
parent 69434 b93404a4c3dd
child 72409 da577e2d42b3
permissions -rwxr-xr-x
more options;
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"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    22
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    23
  echo "  Resolve Isabelle components via download and installation."
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    24
  echo "  COMPONENTS are identified via base name."
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    25
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    26
  echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    27
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    28
  exit 1
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    29
}
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    30
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    31
function fail()
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    32
{
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    33
  echo "$1" >&2
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    34
  exit 2
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    35
}
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    36
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    37
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    38
## process command line
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    39
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    40
#options
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    41
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    42
INIT_SETTINGS=""
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    43
COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    44
ALL_MISSING=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    45
LIST_ONLY=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    46
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    47
while getopts "IR:al" OPT
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    48
do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    49
  case "$OPT" in
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    50
    I)
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    51
      INIT_SETTINGS="true"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    52
      ;;
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    53
    R)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    54
      COMPONENT_REPOSITORY="$OPTARG"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    55
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    56
    a)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    57
      ALL_MISSING="true"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    58
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    59
    l)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    60
      LIST_ONLY="true"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    61
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    62
    \?)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    63
      usage
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    64
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    65
  esac
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    66
done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    67
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    68
shift $(($OPTIND - 1))
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    69
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    70
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    71
# args
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    72
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    73
[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    74
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    75
if [ -z "$ALL_MISSING" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    76
  splitarray ":" "$@"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    77
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    78
  splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    79
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    80
declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    81
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    82
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    83
## main
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    84
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    85
splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    86
splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    87
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    88
if [ -n "$INIT_SETTINGS" ]; then
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    89
  SETTINGS="$ISABELLE_HOME_USER/etc/settings"
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69379
diff changeset
    90
  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
    91
  if [ -e "$SETTINGS" ]; then
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    92
    echo "User settings file already exists!"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    93
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    94
    echo "Edit \"$SETTINGS\" manually"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    95
    echo "and add the following line near its start:"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    96
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    97
    echo "  $SETTINGS_CONTENT"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    98
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    99
  else
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   100
    echo "Initializing \"$SETTINGS\""
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   101
    mkdir -p "$(dirname "$SETTINGS")"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   102
    echo "$SETTINGS_CONTENT" > "$SETTINGS"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   103
  fi
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   104
elif [ -n "$LIST_ONLY" ]; then
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   105
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   106
  echo "Available components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   107
  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   108
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   109
  echo "Missing components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   110
  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   111
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   112
  for NAME in "${SELECTED_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   113
  do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   114
    BASE_NAME="$(basename "$NAME")"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   115
    FULL_NAME=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   116
    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   117
    do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   118
      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   119
    done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   120
    if [ -z "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   121
      echo "Ignoring irrelevant component \"$NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   122
    elif [ -d "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   123
      echo "Skipping existing component \"$FULL_NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   124
    else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   125
      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   126
        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
63490
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 53435
diff changeset
   127
        type -p curl > /dev/null || fail "Cannot download files: missing curl"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   128
        echo "Getting \"$REMOTE\""
48841
90fe0798b83a minor robustification;
wenzelm
parents: 48840
diff changeset
   129
        mkdir -p "$(dirname "$FULL_NAME")"
69379
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   130
        curl --fail --silent "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \
63490
9416333a17c2 prefer curl: presumably more portable and versatile;
wenzelm
parents: 53435
diff changeset
   131
          fail "Failed to download \"$REMOTE\""
69379
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   132
        if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   133
        then
69379
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   134
          rm -f "${FULL_NAME}.tar.gz.part"
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   135
        else
5082e843b726 more robust: avoid broken tar.gz;
wenzelm
parents: 63490
diff changeset
   136
          mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   137
        fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   138
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   139
      if [ -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   140
        echo "Unpacking \"${FULL_NAME}.tar.gz\""
53314
be1c07ec768f check tar error, e.g. from corrupted download;
wenzelm
parents: 50653
diff changeset
   141
        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   142
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   143
    fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   144
  done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   145
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   146