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