lib/Tools/components
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 53435 2220f0fb5581
child 63490 9416333a17c2
permissions -rwxr-xr-x
updated for release;
wenzelm@48840
     1
#!/usr/bin/env bash
wenzelm@48840
     2
#
wenzelm@48840
     3
# Author: Makarius
wenzelm@48840
     4
#
wenzelm@48840
     5
# DESCRIPTION: resolve Isabelle components
wenzelm@48840
     6
wenzelm@48840
     7
wenzelm@48840
     8
## diagnostics
wenzelm@48840
     9
wenzelm@48840
    10
PRG="$(basename "$0")"
wenzelm@48840
    11
wenzelm@48840
    12
function usage()
wenzelm@48840
    13
{
wenzelm@48840
    14
  echo
wenzelm@48840
    15
  echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
wenzelm@48840
    16
  echo
wenzelm@48840
    17
  echo "  Options are:"
wenzelm@50653
    18
  echo "    -I           init user settings"
wenzelm@48840
    19
  echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
wenzelm@53435
    20
  echo "    -a           resolve all missing components"
wenzelm@48840
    21
  echo "    -l           list status"
wenzelm@48840
    22
  echo
wenzelm@48840
    23
  echo "  Resolve Isabelle components via download and installation."
wenzelm@48840
    24
  echo "  COMPONENTS are identified via base name."
wenzelm@48840
    25
  echo
wenzelm@48840
    26
  echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
wenzelm@48840
    27
  echo
wenzelm@48840
    28
  exit 1
wenzelm@48840
    29
}
wenzelm@48840
    30
wenzelm@48840
    31
function fail()
wenzelm@48840
    32
{
wenzelm@48840
    33
  echo "$1" >&2
wenzelm@48840
    34
  exit 2
wenzelm@48840
    35
}
wenzelm@48840
    36
wenzelm@48840
    37
wenzelm@48840
    38
## process command line
wenzelm@48840
    39
wenzelm@48840
    40
#options
wenzelm@48840
    41
wenzelm@50653
    42
INIT_SETTINGS=""
wenzelm@48840
    43
COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
wenzelm@48840
    44
ALL_MISSING=""
wenzelm@48840
    45
LIST_ONLY=""
wenzelm@48840
    46
wenzelm@50653
    47
while getopts "IR:al" OPT
wenzelm@48840
    48
do
wenzelm@48840
    49
  case "$OPT" in
wenzelm@50653
    50
    I)
wenzelm@50653
    51
      INIT_SETTINGS="true"
wenzelm@50653
    52
      ;;
wenzelm@48840
    53
    R)
wenzelm@48840
    54
      COMPONENT_REPOSITORY="$OPTARG"
wenzelm@48840
    55
      ;;
wenzelm@48840
    56
    a)
wenzelm@48840
    57
      ALL_MISSING="true"
wenzelm@48840
    58
      ;;
wenzelm@48840
    59
    l)
wenzelm@48840
    60
      LIST_ONLY="true"
wenzelm@48840
    61
      ;;
wenzelm@48840
    62
    \?)
wenzelm@48840
    63
      usage
wenzelm@48840
    64
      ;;
wenzelm@48840
    65
  esac
wenzelm@48840
    66
done
wenzelm@48840
    67
wenzelm@48840
    68
shift $(($OPTIND - 1))
wenzelm@48840
    69
wenzelm@48840
    70
wenzelm@48840
    71
# args
wenzelm@48840
    72
wenzelm@50653
    73
[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
wenzelm@48840
    74
wenzelm@48840
    75
if [ -z "$ALL_MISSING" ]; then
wenzelm@48840
    76
  splitarray ":" "$@"
wenzelm@48840
    77
else
wenzelm@48840
    78
  splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
wenzelm@48840
    79
fi
wenzelm@48840
    80
declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
wenzelm@48840
    81
wenzelm@48840
    82
wenzelm@48840
    83
## main
wenzelm@48840
    84
wenzelm@48840
    85
splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
wenzelm@48840
    86
splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
wenzelm@48840
    87
wenzelm@50653
    88
if [ -n "$INIT_SETTINGS" ]; then
wenzelm@50653
    89
  SETTINGS="$ISABELLE_HOME_USER/etc/settings"
wenzelm@50653
    90
  SETTINGS_CONTENT='init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"'
wenzelm@50653
    91
  if [ -e "$SETTINGS" ]; then
wenzelm@50653
    92
    echo "User settings file already exists!"
wenzelm@50653
    93
    echo
wenzelm@50653
    94
    echo "Edit \"$SETTINGS\" manually"
wenzelm@50653
    95
    echo "and add the following line near its start:"
wenzelm@50653
    96
    echo
wenzelm@50653
    97
    echo "  $SETTINGS_CONTENT"
wenzelm@50653
    98
    echo
wenzelm@50653
    99
  else
wenzelm@50653
   100
    echo "Initializing \"$SETTINGS\""
wenzelm@50653
   101
    mkdir -p "$(dirname "$SETTINGS")"
wenzelm@50653
   102
    echo "$SETTINGS_CONTENT" > "$SETTINGS"
wenzelm@50653
   103
  fi
wenzelm@50653
   104
elif [ -n "$LIST_ONLY" ]; then
wenzelm@48840
   105
  echo
wenzelm@48840
   106
  echo "Available components:"
wenzelm@48840
   107
  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
wenzelm@48840
   108
  echo
wenzelm@48840
   109
  echo "Missing components:"
wenzelm@48840
   110
  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
wenzelm@48840
   111
else
wenzelm@48840
   112
  for NAME in "${SELECTED_COMPONENTS[@]}"
wenzelm@48840
   113
  do
wenzelm@48840
   114
    BASE_NAME="$(basename "$NAME")"
wenzelm@48840
   115
    FULL_NAME=""
wenzelm@48840
   116
    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
wenzelm@48840
   117
    do
wenzelm@48840
   118
      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
wenzelm@48840
   119
    done
wenzelm@48840
   120
    if [ -z "$FULL_NAME" ]; then
wenzelm@48840
   121
      echo "Ignoring irrelevant component \"$NAME\""
wenzelm@48840
   122
    elif [ -d "$FULL_NAME" ]; then
wenzelm@48840
   123
      echo "Skipping existing component \"$FULL_NAME\""
wenzelm@48840
   124
    else
wenzelm@48840
   125
      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
wenzelm@48840
   126
        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
wenzelm@48840
   127
        echo "Getting \"$REMOTE\""
wenzelm@48841
   128
        mkdir -p "$(dirname "$FULL_NAME")"
wenzelm@48840
   129
        perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"
wenzelm@48840
   130
        if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
wenzelm@48840
   131
        then
wenzelm@48840
   132
          rm -f "${FULL_NAME}.tar.gz"
wenzelm@48840
   133
        fi
wenzelm@48840
   134
      fi
wenzelm@48840
   135
      if [ -e "${FULL_NAME}.tar.gz" ]; then
wenzelm@48840
   136
        echo "Unpacking \"${FULL_NAME}.tar.gz\""
wenzelm@53314
   137
        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
wenzelm@48840
   138
      fi
wenzelm@48840
   139
    fi
wenzelm@48840
   140
  done
wenzelm@48840
   141
fi
wenzelm@48840
   142