lib/Tools/components
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 50653 5c85f8b80b95
child 53314 be1c07ec768f
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     2
#
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     4
#
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: resolve Isabelle components
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     6
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     7
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     8
## diagnostics
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
     9
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    11
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    12
function usage()
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    13
{
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    14
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    16
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    18
  echo "    -I           init user settings"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    19
  echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    20
  echo "    -a           all missing components"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    21
  echo "    -l           list status"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    22
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    23
  echo "  Resolve Isabelle components via download and installation."
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    24
  echo "  COMPONENTS are identified via base name."
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    25
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    26
  echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    27
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    28
  exit 1
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    29
}
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    30
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    31
function fail()
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    32
{
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    33
  echo "$1" >&2
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    34
  exit 2
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    35
}
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    36
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    37
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    38
## process command line
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    39
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    40
#options
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    41
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    42
INIT_SETTINGS=""
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    43
COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    44
ALL_MISSING=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    45
LIST_ONLY=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    46
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    47
while getopts "IR:al" OPT
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    48
do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    49
  case "$OPT" in
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    50
    I)
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    51
      INIT_SETTINGS="true"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    52
      ;;
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    53
    R)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    54
      COMPONENT_REPOSITORY="$OPTARG"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    55
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    56
    a)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    57
      ALL_MISSING="true"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    58
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    59
    l)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    60
      LIST_ONLY="true"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    61
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    62
    \?)
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    63
      usage
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    64
      ;;
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    65
  esac
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    66
done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    67
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    68
shift $(($OPTIND - 1))
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    69
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    70
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    71
# args
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    72
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    73
[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    74
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    75
if [ -z "$ALL_MISSING" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    76
  splitarray ":" "$@"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    77
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    78
  splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    79
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    80
declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    81
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    82
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    83
## main
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    84
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    85
splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    86
splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
    87
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    88
if [ -n "$INIT_SETTINGS" ]; then
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    89
  SETTINGS="$ISABELLE_HOME_USER/etc/settings"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    90
  SETTINGS_CONTENT='init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"'
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    91
  if [ -e "$SETTINGS" ]; then
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    92
    echo "User settings file already exists!"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    93
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    94
    echo "Edit \"$SETTINGS\" manually"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    95
    echo "and add the following line near its start:"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    96
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    97
    echo "  $SETTINGS_CONTENT"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    98
    echo
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
    99
  else
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   100
    echo "Initializing \"$SETTINGS\""
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   101
    mkdir -p "$(dirname "$SETTINGS")"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   102
    echo "$SETTINGS_CONTENT" > "$SETTINGS"
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   103
  fi
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 48841
diff changeset
   104
elif [ -n "$LIST_ONLY" ]; then
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   105
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   106
  echo "Available components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   107
  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   108
  echo
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   109
  echo "Missing components:"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   110
  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   111
else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   112
  for NAME in "${SELECTED_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   113
  do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   114
    BASE_NAME="$(basename "$NAME")"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   115
    FULL_NAME=""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   116
    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   117
    do
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   118
      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   119
    done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   120
    if [ -z "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   121
      echo "Ignoring irrelevant component \"$NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   122
    elif [ -d "$FULL_NAME" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   123
      echo "Skipping existing component \"$FULL_NAME\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   124
    else
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   125
      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   126
        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   127
        echo "Getting \"$REMOTE\""
48841
90fe0798b83a minor robustification;
wenzelm
parents: 48840
diff changeset
   128
        mkdir -p "$(dirname "$FULL_NAME")"
48840
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   129
        perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   130
        if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   131
        then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   132
          rm -f "${FULL_NAME}.tar.gz"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   133
        fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   134
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   135
      if [ -e "${FULL_NAME}.tar.gz" ]; then
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   136
        echo "Unpacking \"${FULL_NAME}.tar.gz\""
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   137
        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz"
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   138
      fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   139
    fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   140
  done
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   141
fi
7e19dc018db9 added "isabelle components" tool;
wenzelm
parents:
diff changeset
   142