added "isabelle components" tool;
authorwenzelm
Fri Aug 17 14:56:37 2012 +0200 (2012-08-17)
changeset 488407e19dc018db9
parent 48839 f49745d1395a
child 48841 90fe0798b83a
added "isabelle components" tool;
etc/settings
lib/Tools/components
     1.1 --- a/etc/settings	Fri Aug 17 14:55:46 2012 +0200
     1.2 +++ b/etc/settings	Fri Aug 17 14:56:37 2012 +0200
     1.3 @@ -96,6 +96,8 @@
     1.4  ### Misc path settings
     1.5  ###
     1.6  
     1.7 +ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
     1.8 +
     1.9  # The place for user configuration, heap files, etc.
    1.10  if [ -z "$ISABELLE_IDENTIFIER" ]; then
    1.11    ISABELLE_HOME_USER="$USER_HOME/.isabelle"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/Tools/components	Fri Aug 17 14:56:37 2012 +0200
     2.3 @@ -0,0 +1,120 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# Author: Makarius
     2.7 +#
     2.8 +# DESCRIPTION: resolve Isabelle components
     2.9 +
    2.10 +
    2.11 +## diagnostics
    2.12 +
    2.13 +PRG="$(basename "$0")"
    2.14 +
    2.15 +function usage()
    2.16 +{
    2.17 +  echo
    2.18 +  echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
    2.19 +  echo
    2.20 +  echo "  Options are:"
    2.21 +  echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
    2.22 +  echo "    -a           all missing components"
    2.23 +  echo "    -l           list status"
    2.24 +  echo
    2.25 +  echo "  Resolve Isabelle components via download and installation."
    2.26 +  echo "  COMPONENTS are identified via base name."
    2.27 +  echo
    2.28 +  echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
    2.29 +  echo
    2.30 +  exit 1
    2.31 +}
    2.32 +
    2.33 +function fail()
    2.34 +{
    2.35 +  echo "$1" >&2
    2.36 +  exit 2
    2.37 +}
    2.38 +
    2.39 +
    2.40 +## process command line
    2.41 +
    2.42 +#options
    2.43 +
    2.44 +COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
    2.45 +ALL_MISSING=""
    2.46 +LIST_ONLY=""
    2.47 +
    2.48 +while getopts "R:al" OPT
    2.49 +do
    2.50 +  case "$OPT" in
    2.51 +    R)
    2.52 +      COMPONENT_REPOSITORY="$OPTARG"
    2.53 +      ;;
    2.54 +    a)
    2.55 +      ALL_MISSING="true"
    2.56 +      ;;
    2.57 +    l)
    2.58 +      LIST_ONLY="true"
    2.59 +      ;;
    2.60 +    \?)
    2.61 +      usage
    2.62 +      ;;
    2.63 +  esac
    2.64 +done
    2.65 +
    2.66 +shift $(($OPTIND - 1))
    2.67 +
    2.68 +
    2.69 +# args
    2.70 +
    2.71 +[ "$#" -eq 0 -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
    2.72 +
    2.73 +if [ -z "$ALL_MISSING" ]; then
    2.74 +  splitarray ":" "$@"
    2.75 +else
    2.76 +  splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
    2.77 +fi
    2.78 +declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
    2.79 +
    2.80 +
    2.81 +## main
    2.82 +
    2.83 +splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
    2.84 +splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
    2.85 +
    2.86 +if [ -n "$LIST_ONLY" ]; then
    2.87 +  echo
    2.88 +  echo "Available components:"
    2.89 +  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
    2.90 +  echo
    2.91 +  echo "Missing components:"
    2.92 +  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
    2.93 +else
    2.94 +  for NAME in "${SELECTED_COMPONENTS[@]}"
    2.95 +  do
    2.96 +    BASE_NAME="$(basename "$NAME")"
    2.97 +    FULL_NAME=""
    2.98 +    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
    2.99 +    do
   2.100 +      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
   2.101 +    done
   2.102 +    if [ -z "$FULL_NAME" ]; then
   2.103 +      echo "Ignoring irrelevant component \"$NAME\""
   2.104 +    elif [ -d "$FULL_NAME" ]; then
   2.105 +      echo "Skipping existing component \"$FULL_NAME\""
   2.106 +    else
   2.107 +      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
   2.108 +        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
   2.109 +        echo "Getting \"$REMOTE\""
   2.110 +        perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"
   2.111 +        if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
   2.112 +        then
   2.113 +          rm -f "${FULL_NAME}.tar.gz"
   2.114 +        fi
   2.115 +      fi
   2.116 +      if [ -e "${FULL_NAME}.tar.gz" ]; then
   2.117 +        echo "Unpacking \"${FULL_NAME}.tar.gz\""
   2.118 +        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz"
   2.119 +      fi
   2.120 +    fi
   2.121 +  done
   2.122 +fi
   2.123 +