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