lib/Tools/components

don't early error on SMT_Failure.Other_Failure

Otherwise, `by (smt A | metis B)` would fail if `smt A` fails with Other_Failure, even if `metis B` would succeed.

#!/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
  source "$ISABELLE_HOME/lib/scripts/download_file"
  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
        download_file "$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz" "${FULL_NAME}.tar.gz" || exit $?
      fi
      if [ -e "${FULL_NAME}.tar.gz" ]; then
        echo "Unpacking \"${FULL_NAME}.tar.gz\""
        tar -C "$(dirname "$FULL_NAME")" -x -z -f "${FULL_NAME}.tar.gz" || exit 2
      fi
    fi
  done
fi