diff --git a/lib/Tools/components b/lib/Tools/components --- a/lib/Tools/components +++ b/lib/Tools/components @@ -1,146 +1,150 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: resolve Isabelle components ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]" echo echo " Options are:" echo " -I init user settings" echo " -R URL component repository (default \$ISABELLE_COMPONENT_REPOSITORY)" echo " -a resolve all missing components" echo " -l list status" echo echo " Resolve Isabelle components via download and installation." echo " COMPONENTS are identified via base name." echo echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\"" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } ## process command line #options INIT_SETTINGS="" COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY" ALL_MISSING="" LIST_ONLY="" while getopts "IR:al" OPT do case "$OPT" in I) INIT_SETTINGS="true" ;; R) COMPONENT_REPOSITORY="$OPTARG" ;; a) ALL_MISSING="true" ;; l) LIST_ONLY="true" ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage if [ -z "$ALL_MISSING" ]; then splitarray ":" "$@" else splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@" fi declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}") ## main splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}") splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}") if [ -n "$INIT_SETTINGS" ]; then SETTINGS="$ISABELLE_HOME_USER/etc/settings" SETTINGS_CONTENT='init_components "$ISABELLE_COMPONENTS_BASE" "$ISABELLE_HOME/Admin/components/main"' if [ -e "$SETTINGS" ]; then echo "User settings file already exists!" echo echo "Edit \"$SETTINGS\" manually" echo "and add the following line near its start:" echo echo " $SETTINGS_CONTENT" echo else echo "Initializing \"$SETTINGS\"" mkdir -p "$(dirname "$SETTINGS")" - echo "$SETTINGS_CONTENT" > "$SETTINGS" + { + echo "#-*- shell-script -*- :mode=shellscript:" + echo + echo "$SETTINGS_CONTENT" + } > "$SETTINGS" fi elif [ -n "$LIST_ONLY" ]; then echo echo "Available components:" for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo " $NAME"; done echo echo "Missing components:" for NAME in "${MISSING_COMPONENTS[@]}"; do echo " $NAME"; done else for NAME in "${SELECTED_COMPONENTS[@]}" do BASE_NAME="$(basename "$NAME")" FULL_NAME="" for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}" do [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X" done if [ -z "$FULL_NAME" ]; then echo "Ignoring irrelevant component \"$NAME\"" elif [ -d "$FULL_NAME" ]; then echo "Skipping existing component \"$FULL_NAME\"" else if [ ! -e "${FULL_NAME}.tar.gz" ]; then REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz" type -p curl > /dev/null || fail "Cannot download files: missing curl" echo "Getting \"$REMOTE\"" mkdir -p "$(dirname "$FULL_NAME")" curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \ fail "Failed to download \"$REMOTE\"" if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);" then rm -f "${FULL_NAME}.tar.gz.part" else mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz" fi fi if [ -e "${FULL_NAME}.tar.gz" ]; then echo "Unpacking \"${FULL_NAME}.tar.gz\"" tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2 fi fi done fi