1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Florian Haftmann |
|
4 # Author: Tjark Weber |
|
5 # |
|
6 # Download and unpack Isabelle components from central component store. |
|
7 |
|
8 shopt -s -o errexit |
|
9 shopt -s -o nounset |
|
10 |
|
11 REMOTE='http://isabelle.in.tum.de/components' |
|
12 |
|
13 ## diagnostics |
|
14 |
|
15 PRG="$(basename "$0")" |
|
16 |
|
17 trap 'echo "Error in ${PRG}" >&2' ERR |
|
18 |
|
19 function usage() |
|
20 { |
|
21 cat <<EOF |
|
22 |
|
23 Usage: ${PRG} [OPTIONS] [COMPONENTS ...] |
|
24 |
|
25 Options are: |
|
26 -c Download current components (as listed in Admin/components). |
|
27 -q Quiet (do not output diagnostic messages). |
|
28 -r Replace components already present (default is to skip). |
|
29 -x Exit on failed download (default is to ignore). |
|
30 |
|
31 Download and unpack Isabelle components from central component store |
|
32 (${REMOTE}/). |
|
33 |
|
34 EOF |
|
35 exit 1 |
|
36 } |
|
37 |
|
38 function fail() |
|
39 { |
|
40 echo "$1" >&2 |
|
41 exit 2 |
|
42 } |
|
43 |
|
44 ## process command line |
|
45 |
|
46 # options |
|
47 |
|
48 DOWNLOAD_CURRENT="" |
|
49 ECHO="echo" |
|
50 REPLACE_EXISTING="" |
|
51 EXIT_ON_FAILED_DOWNLOAD="" |
|
52 |
|
53 function getoptions() |
|
54 { |
|
55 OPTIND=1 |
|
56 while getopts "cqrx" OPT |
|
57 do |
|
58 case "$OPT" in |
|
59 c) |
|
60 DOWNLOAD_CURRENT=true |
|
61 ;; |
|
62 q) |
|
63 ECHO=":" |
|
64 ;; |
|
65 r) |
|
66 REPLACE_EXISTING=true |
|
67 ;; |
|
68 x) |
|
69 EXIT_ON_FAILED_DOWNLOAD=true |
|
70 ;; |
|
71 \?) |
|
72 usage |
|
73 ;; |
|
74 esac |
|
75 done |
|
76 } |
|
77 |
|
78 getoptions "$@" |
|
79 shift $(($OPTIND - 1)) |
|
80 |
|
81 ## directory layout |
|
82 |
|
83 : ${TMPDIR:="/tmp"} |
|
84 |
|
85 : ${ISABELLE_HOME_USER:=""} |
|
86 |
|
87 if [ -z "${ISABELLE_HOME_USER}" ]; then |
|
88 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
|
89 ISABELLE_TOOL="${ISABELLE_HOME}/bin/isabelle" |
|
90 ISABELLE_HOME_USER="$("${ISABELLE_TOOL}" getenv -b ISABELLE_HOME_USER)" |
|
91 fi |
|
92 |
|
93 LOCAL="${ISABELLE_HOME_USER}/contrib" |
|
94 |
|
95 ## download (and unpack) components |
|
96 |
|
97 function download() |
|
98 { |
|
99 if [ -e "${LOCAL}/${COMPONENT}" -a -z "${REPLACE_EXISTING}" ]; then |
|
100 "${ECHO}" "Skipping existing component ${COMPONENT}" |
|
101 else |
|
102 "${ECHO}" "${COMPONENT}" |
|
103 ARCHIVE="${COMPONENT}.tar.gz" |
|
104 if curl -s `"${ECHO}" --no-silent` -f -o "${TMPDIR}/${ARCHIVE}" "${REMOTE}/${ARCHIVE}"; then |
|
105 tar -xzf "${TMPDIR}/${ARCHIVE}" -C "${LOCAL}" --recursive-unlink |
|
106 else |
|
107 if [ -n "${EXIT_ON_FAILED_DOWNLOAD}" ]; then |
|
108 fail "Error downloading component ${COMPONENT} (non-free?)" |
|
109 else |
|
110 "${ECHO}" "Error downloading component ${COMPONENT} (non-free?)" |
|
111 fi |
|
112 fi |
|
113 fi |
|
114 } |
|
115 |
|
116 "${ECHO}" "Unpacking components into ${LOCAL}/" |
|
117 |
|
118 [ -e "${LOCAL}" ] || mkdir -p "${LOCAL}" |
|
119 |
|
120 # process Admin/components |
|
121 if [ -n "${DOWNLOAD_CURRENT}" ]; then |
|
122 while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; } |
|
123 do |
|
124 case "${REPLY}" in |
|
125 \#* | "") |
|
126 ;; |
|
127 *) |
|
128 COMPONENT="$(basename "${REPLY}")" |
|
129 download "${COMPONENT}" |
|
130 ;; |
|
131 esac |
|
132 done < "$ISABELLE_HOME/Admin/components" |
|
133 fi |
|
134 |
|
135 # process args |
|
136 for COMPONENT in "$@" |
|
137 do |
|
138 download "${COMPONENT}" |
|
139 done |
|