lib/Tools/components
author wenzelm
Fri, 17 Aug 2012 14:56:37 +0200
changeset 48840 7e19dc018db9
child 48841 90fe0798b83a
permissions -rwxr-xr-x
added "isabelle components" tool;
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:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    18
  echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    19
  echo "    -a           all missing components"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    20
  echo "    -l           list status"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    21
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    22
  echo "  Resolve Isabelle components via download and installation."
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    23
  echo "  COMPONENTS are identified via base name."
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    24
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    25
  echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    26
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    27
  exit 1
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    28
}
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    29
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    30
function fail()
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    31
{
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    32
  echo "$1" >&2
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    33
  exit 2
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    34
}
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
## process command line
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    38
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    39
#options
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    40
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    41
COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    42
ALL_MISSING=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    43
LIST_ONLY=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    44
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    45
while getopts "R:al" OPT
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    46
do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    47
  case "$OPT" in
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    48
    R)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    49
      COMPONENT_REPOSITORY="$OPTARG"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    50
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    51
    a)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    52
      ALL_MISSING="true"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    53
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    54
    l)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    55
      LIST_ONLY="true"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    56
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    57
    \?)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    58
      usage
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    59
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    60
  esac
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    61
done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    62
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    63
shift $(($OPTIND - 1))
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    64
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    65
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    66
# args
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    67
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    68
[ "$#" -eq 0 -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    69
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    70
if [ -z "$ALL_MISSING" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    71
  splitarray ":" "$@"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    72
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    73
  splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    74
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    75
declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    76
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    77
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    78
## main
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    79
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    80
splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    81
splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    82
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    83
if [ -n "$LIST_ONLY" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    84
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    85
  echo "Available components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    86
  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    87
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    88
  echo "Missing components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    89
  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    90
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    91
  for NAME in "${SELECTED_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    92
  do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    93
    BASE_NAME="$(basename "$NAME")"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    94
    FULL_NAME=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    95
    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    96
    do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    97
      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    98
    done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    99
    if [ -z "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   100
      echo "Ignoring irrelevant component \"$NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   101
    elif [ -d "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   102
      echo "Skipping existing component \"$FULL_NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   103
    else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   104
      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   105
        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   106
        echo "Getting \"$REMOTE\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   107
        perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   108
        if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   109
        then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   110
          rm -f "${FULL_NAME}.tar.gz"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   111
        fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   112
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   113
      if [ -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   114
        echo "Unpacking \"${FULL_NAME}.tar.gz\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   115
        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   116
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   117
    fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   118
  done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   119
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   120