author | wenzelm |
Thu, 21 Jan 2021 16:10:43 +0100 | |
changeset 73172 | fc828f64da5b |
parent 72524 | 8e9312e6a6d9 |
child 73308 | f73c691bd679 |
permissions | -rwxr-xr-x |
48840 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# Author: Makarius |
|
4 |
# |
|
5 |
# DESCRIPTION: resolve Isabelle components |
|
6 |
||
7 |
||
8 |
## diagnostics |
|
9 |
||
10 |
PRG="$(basename "$0")" |
|
11 |
||
12 |
function usage() |
|
13 |
{ |
|
14 |
echo |
|
15 |
echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]" |
|
16 |
echo |
|
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 | 19 |
echo " -R URL component repository (default \$ISABELLE_COMPONENT_REPOSITORY)" |
53435 | 20 |
echo " -a resolve all missing components" |
48840 | 21 |
echo " -l list status" |
73172 | 22 |
echo " -u DIR update \$ISABELLE_HOME_USER/components: add directory" |
23 |
echo " -x DIR update \$ISABELLE_HOME_USER/components: remove directory" |
|
48840 | 24 |
echo |
73172 | 25 |
echo " Resolve Isabelle components via download and installation: given COMPONENTS" |
26 |
echo " are identified via base name. Further operations manage etc/settings and" |
|
27 |
echo " etc/components in \$ISABELLE_HOME_USER." |
|
48840 | 28 |
echo |
29 |
echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\"" |
|
73172 | 30 |
echo " ISABELLE_HOME_USER=\"$ISABELLE_HOME_USER\"" |
48840 | 31 |
echo |
32 |
exit 1 |
|
33 |
} |
|
34 |
||
35 |
function fail() |
|
36 |
{ |
|
37 |
echo "$1" >&2 |
|
38 |
exit 2 |
|
39 |
} |
|
40 |
||
41 |
||
42 |
## process command line |
|
43 |
||
44 |
#options |
|
45 |
||
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
46 |
INIT_SETTINGS="" |
48840 | 47 |
COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY" |
48 |
ALL_MISSING="" |
|
49 |
LIST_ONLY="" |
|
73172 | 50 |
declare -a UPDATE_COMPONENTS=() |
48840 | 51 |
|
73172 | 52 |
while getopts "IR:alu:x:" OPT |
48840 | 53 |
do |
54 |
case "$OPT" in |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
55 |
I) |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
56 |
INIT_SETTINGS="true" |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
57 |
;; |
48840 | 58 |
R) |
59 |
COMPONENT_REPOSITORY="$OPTARG" |
|
60 |
;; |
|
61 |
a) |
|
62 |
ALL_MISSING="true" |
|
63 |
;; |
|
64 |
l) |
|
65 |
LIST_ONLY="true" |
|
66 |
;; |
|
73172 | 67 |
u) |
68 |
UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="+$OPTARG" |
|
69 |
;; |
|
70 |
x) |
|
71 |
UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="-$OPTARG" |
|
72 |
;; |
|
48840 | 73 |
\?) |
74 |
usage |
|
75 |
;; |
|
76 |
esac |
|
77 |
done |
|
78 |
||
79 |
shift $(($OPTIND - 1)) |
|
80 |
||
81 |
||
82 |
# args |
|
83 |
||
73172 | 84 |
[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" -a "${#UPDATE_COMPONENTS[@]}" -eq 0 ] && usage |
48840 | 85 |
|
86 |
if [ -z "$ALL_MISSING" ]; then |
|
87 |
splitarray ":" "$@" |
|
88 |
else |
|
89 |
splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@" |
|
90 |
fi |
|
91 |
declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}") |
|
92 |
||
93 |
||
94 |
## main |
|
95 |
||
96 |
splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}") |
|
97 |
splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}") |
|
98 |
||
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
99 |
if [ -n "$INIT_SETTINGS" ]; then |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
100 |
SETTINGS="$ISABELLE_HOME_USER/etc/settings" |
69434 | 101 |
SETTINGS_CONTENT='init_components "$ISABELLE_COMPONENTS_BASE" "$ISABELLE_HOME/Admin/components/main"' |
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
102 |
if [ -e "$SETTINGS" ]; then |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
103 |
echo "User settings file already exists!" |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
104 |
echo |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
105 |
echo "Edit \"$SETTINGS\" manually" |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
106 |
echo "and add the following line near its start:" |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
107 |
echo |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
108 |
echo " $SETTINGS_CONTENT" |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
109 |
echo |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
110 |
else |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
111 |
echo "Initializing \"$SETTINGS\"" |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
112 |
mkdir -p "$(dirname "$SETTINGS")" |
72524 | 113 |
{ |
114 |
echo "#-*- shell-script -*- :mode=shellscript:" |
|
115 |
echo |
|
116 |
echo "$SETTINGS_CONTENT" |
|
117 |
} > "$SETTINGS" |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
118 |
fi |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
48841
diff
changeset
|
119 |
elif [ -n "$LIST_ONLY" ]; then |
48840 | 120 |
echo |
121 |
echo "Available components:" |
|
122 |
for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo " $NAME"; done |
|
123 |
echo |
|
124 |
echo "Missing components:" |
|
125 |
for NAME in "${MISSING_COMPONENTS[@]}"; do echo " $NAME"; done |
|
73172 | 126 |
elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then |
127 |
isabelle_admin_build jars || exit $? |
|
128 |
exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}" |
|
48840 | 129 |
else |
130 |
for NAME in "${SELECTED_COMPONENTS[@]}" |
|
131 |
do |
|
132 |
BASE_NAME="$(basename "$NAME")" |
|
133 |
FULL_NAME="" |
|
134 |
for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}" |
|
135 |
do |
|
136 |
[ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X" |
|
137 |
done |
|
138 |
if [ -z "$FULL_NAME" ]; then |
|
139 |
echo "Ignoring irrelevant component \"$NAME\"" |
|
140 |
elif [ -d "$FULL_NAME" ]; then |
|
141 |
echo "Skipping existing component \"$FULL_NAME\"" |
|
142 |
else |
|
143 |
if [ ! -e "${FULL_NAME}.tar.gz" ]; then |
|
144 |
REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz" |
|
63490
9416333a17c2
prefer curl: presumably more portable and versatile;
wenzelm
parents:
53435
diff
changeset
|
145 |
type -p curl > /dev/null || fail "Cannot download files: missing curl" |
48840 | 146 |
echo "Getting \"$REMOTE\"" |
48841 | 147 |
mkdir -p "$(dirname "$FULL_NAME")" |
72409 | 148 |
curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \ |
63490
9416333a17c2
prefer curl: presumably more portable and versatile;
wenzelm
parents:
53435
diff
changeset
|
149 |
fail "Failed to download \"$REMOTE\"" |
69379 | 150 |
if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);" |
48840 | 151 |
then |
69379 | 152 |
rm -f "${FULL_NAME}.tar.gz.part" |
153 |
else |
|
154 |
mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz" |
|
48840 | 155 |
fi |
156 |
fi |
|
157 |
if [ -e "${FULL_NAME}.tar.gz" ]; then |
|
158 |
echo "Unpacking \"${FULL_NAME}.tar.gz\"" |
|
53314 | 159 |
tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2 |
48840 | 160 |
fi |
161 |
fi |
|
162 |
done |
|
163 |
fi |
|
164 |