1#!/usr/bin/env bash 2# 3# Author: Makarius 4# 5# DESCRIPTION: resolve Isabelle components 6 7 8## diagnostics 9 10PRG="$(basename "$0")" 11 12function 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 31function fail() 32{ 33 echo "$1" >&2 34 exit 2 35} 36 37 38## process command line 39 40#options 41 42INIT_SETTINGS="" 43COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY" 44ALL_MISSING="" 45LIST_ONLY="" 46 47while getopts "IR:al" OPT 48do 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 66done 67 68shift $(($OPTIND - 1)) 69 70 71# args 72 73[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage 74 75if [ -z "$ALL_MISSING" ]; then 76 splitarray ":" "$@" 77else 78 splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@" 79fi 80declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}") 81 82 83## main 84 85splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}") 86splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}") 87 88if [ -n "$INIT_SETTINGS" ]; then 89 SETTINGS="$ISABELLE_HOME_USER/etc/settings" 90 SETTINGS_CONTENT='init_components "$ISABELLE_COMPONENTS_BASE" "$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 104elif [ -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 111else 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.part" || \ 131 fail "Failed to download \"$REMOTE\"" 132 if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);" 133 then 134 rm -f "${FULL_NAME}.tar.gz.part" 135 else 136 mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz" 137 fi 138 fi 139 if [ -e "${FULL_NAME}.tar.gz" ]; then 140 echo "Unpacking \"${FULL_NAME}.tar.gz\"" 141 tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2 142 fi 143 fi 144 done 145fi 146 147