wneuper/isa: lib/Tools/components@2220f0fb5581

     1 #!/usr/bin/env bash

2 #

     3 # Author: Makarius

4 #

     5 # DESCRIPTION: resolve Isabelle components

     8 ## diagnostics

    10 PRG="$(basename "$0")"

    12 function usage()

    13 {

    14   echo

    15   echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"

    16   echo

    17   echo "  Options are:"

    18   echo "    -I           init user settings"

    19   echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"

    20   echo "    -a           resolve all missing components"

    21   echo "    -l           list status"

    22   echo

    23   echo "  Resolve Isabelle components via download and installation."

    24   echo "  COMPONENTS are identified via base name."

    25   echo

    26   echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""

    27   echo

    28   exit 1

    29 }

    31 function fail()

    32 {

    33   echo "$1" >&2

    34   exit 2

    35 }

    38 ## process command line

    40 #options

    42 INIT_SETTINGS=""

    43 COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"

    44 ALL_MISSING=""

    45 LIST_ONLY=""

    47 while getopts "IR:al" OPT

    48 do

    49   case "$OPT" in

    50     I)

    51       INIT_SETTINGS="true"

    52       ;;

    53     R)

    54       COMPONENT_REPOSITORY="$OPTARG"

    55       ;;

    56     a)

    57       ALL_MISSING="true"

    58       ;;

    59     l)

    60       LIST_ONLY="true"

    61       ;;

    62     \?)

    63       usage

    64       ;;

    65   esac

    66 done

    68 shift $(($OPTIND - 1))

    71 # args

    73 [ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage

    75 if [ -z "$ALL_MISSING" ]; then

    76   splitarray ":" "$@"

    77 else

    78   splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"

    79 fi

    80 declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")

    83 ## main

    85 splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")

    86 splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")

    88 if [ -n "$INIT_SETTINGS" ]; then

    89   SETTINGS="$ISABELLE_HOME_USER/etc/settings"

    90   SETTINGS_CONTENT='init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"'

    91   if [ -e "$SETTINGS" ]; then

    92     echo "User settings file already exists!"

    93     echo

    94     echo "Edit \"$SETTINGS\" manually"

    95     echo "and add the following line near its start:"

    96     echo

    97     echo "  $SETTINGS_CONTENT"

    98     echo

    99   else

   100     echo "Initializing \"$SETTINGS\""

   101     mkdir -p "$(dirname "$SETTINGS")"

   102     echo "$SETTINGS_CONTENT" > "$SETTINGS"

   103   fi

   104 elif [ -n "$LIST_ONLY" ]; then

   105   echo

   106   echo "Available components:"

   107   for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done

   108   echo

   109   echo "Missing components:"

   110   for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done

   111 else

   112   for NAME in "${SELECTED_COMPONENTS[@]}"

   113   do

   114     BASE_NAME="$(basename "$NAME")"

   115     FULL_NAME=""

   116     for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"

   117     do

   118       [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"

   119     done

   120     if [ -z "$FULL_NAME" ]; then

   121       echo "Ignoring irrelevant component \"$NAME\""

   122     elif [ -d "$FULL_NAME" ]; then

   123       echo "Skipping existing component \"$FULL_NAME\""

   124     else

   125       if [ ! -e "${FULL_NAME}.tar.gz" ]; then

   126         REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"

   127         echo "Getting \"$REMOTE\""

   128         mkdir -p "$(dirname "$FULL_NAME")"

   129         perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"

   130         if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"

   131         then

   132           rm -f "${FULL_NAME}.tar.gz"

   133         fi

   134       fi

   135       if [ -e "${FULL_NAME}.tar.gz" ]; then

   136         echo "Unpacking \"${FULL_NAME}.tar.gz\""

   137         tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2

   138       fi

   139     fi

   140   done

   141 fi

author	wenzelm
	Fri, 06 Sep 2013 12:46:50 +0200
changeset 54572	2220f0fb5581
parent 54451	be1c07ec768f
child 59324	ec559c6ab5ba
permissions	-rwxr-xr-x