diff --git a/lib/Tools/components b/lib/Tools/components --- a/lib/Tools/components +++ b/lib/Tools/components @@ -1,166 +1,175 @@ #!/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 " -u DIR update \$ISABELLE_HOME_USER/etc/components: add directory" echo " -x DIR update \$ISABELLE_HOME_USER/etc/components: remove directory" echo echo " Resolve Isabelle components via download and installation: given COMPONENTS" echo " are identified via base name. Further operations manage etc/settings and" echo " etc/components in \$ISABELLE_HOME_USER." echo echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\"" echo " ISABELLE_HOME_USER=\"$ISABELLE_HOME_USER\"" 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="" declare -a UPDATE_COMPONENTS=() while getopts "IR:alu:x:" OPT do case "$OPT" in I) INIT_SETTINGS="true" ;; R) COMPONENT_REPOSITORY="$OPTARG" ;; a) ALL_MISSING="true" ;; l) LIST_ONLY="true" ;; u) UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="+$OPTARG" ;; x) UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="-$OPTARG" ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" -a "${#UPDATE_COMPONENTS[@]}" -eq 0 ] && 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:-$USER_HOME/.isabelle/contrib}" "$ISABELLE_HOME/Admin/components/main"' if [ ! -e "$SETTINGS" ]; then echo "Initializing \"$SETTINGS\"" mkdir -p "$(dirname "$SETTINGS")" { echo "#-*- shell-script -*- :mode=shellscript:" echo echo "$SETTINGS_CONTENT" } > "$SETTINGS" elif grep "init_components.*components/main" "$SETTINGS" >/dev/null 2>/dev/null then : else 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 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 elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then isabelle scala_build || exit $? exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}" 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")" - if curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part" + + CURL_OPTIONS="--fail --silent --location" + if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then + case $(sw_vers -productVersion) in + 10.*) + CURL_OPTIONS="$CURL_OPTIONS --insecure" + ;; + esac + fi + if curl $CURL_OPTIONS "$REMOTE" > "${FULL_NAME}.tar.gz.part" then mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz" else rm -f "${FULL_NAME}.tar.gz.part" fail "Failed to download \"$REMOTE\"" 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