lib/Tools/components
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 63490 9416333a17c2
child 69379 5082e843b726
permissions -rwxr-xr-x
more robust sorted_entries;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # DESCRIPTION: resolve Isabelle components
     6 
     7 
     8 ## diagnostics
     9 
    10 PRG="$(basename "$0")"
    11 
    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 }
    30 
    31 function fail()
    32 {
    33   echo "$1" >&2
    34   exit 2
    35 }
    36 
    37 
    38 ## process command line
    39 
    40 #options
    41 
    42 INIT_SETTINGS=""
    43 COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
    44 ALL_MISSING=""
    45 LIST_ONLY=""
    46 
    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
    67 
    68 shift $(($OPTIND - 1))
    69 
    70 
    71 # args
    72 
    73 [ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
    74 
    75 if [ -z "$ALL_MISSING" ]; then
    76   splitarray ":" "$@"
    77 else
    78   splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
    79 fi
    80 declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
    81 
    82 
    83 ## main
    84 
    85 splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
    86 splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
    87 
    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         type -p curl > /dev/null || fail "Cannot download files: missing curl"
   128         echo "Getting \"$REMOTE\""
   129         mkdir -p "$(dirname "$FULL_NAME")"
   130         curl --fail --silent "$REMOTE" > "${FULL_NAME}.tar.gz" || \
   131           fail "Failed to download \"$REMOTE\""
   132         if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
   133         then
   134           rm -f "${FULL_NAME}.tar.gz"
   135         fi
   136       fi
   137       if [ -e "${FULL_NAME}.tar.gz" ]; then
   138         echo "Unpacking \"${FULL_NAME}.tar.gz\""
   139         tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
   140       fi
   141     fi
   142   done
   143 fi
   144