1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Makarius |
|
4 # |
|
5 # DESCRIPTION: setup for Isabelle repository clone or repository archive |
|
6 |
|
7 |
|
8 ## diagnostics |
|
9 |
|
10 PRG="$(basename "$0")" |
|
11 |
|
12 ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle" |
|
13 |
|
14 function usage() |
|
15 { |
|
16 echo |
|
17 echo "Usage: isabelle $PRG [OPTIONS]" |
|
18 echo |
|
19 echo " Options are:" |
|
20 echo " -C enforce clean update of working directory (no backup!)" |
|
21 echo " -R version is current official release" |
|
22 echo " -U URL Isabelle repository server (default: \"$ISABELLE_REPOS\")" |
|
23 echo " -V PATH version from explicit file or directory (file \"ISABELLE_VERSION\")" |
|
24 echo " -r REV version according to Mercurial notation" |
|
25 echo " -u version is remote tip" |
|
26 echo |
|
27 echo " Setup the current ISABELLE_HOME directory, which needs to be a" |
|
28 echo " repository clone (all versions) or repository archive (fixed version)." |
|
29 echo |
|
30 exit 1 |
|
31 } |
|
32 |
|
33 function fail() |
|
34 { |
|
35 echo "$1" >&2 |
|
36 exit 2 |
|
37 } |
|
38 |
|
39 |
|
40 ## process command line |
|
41 |
|
42 #options |
|
43 |
|
44 CLEAN="" |
|
45 |
|
46 VERSION="" |
|
47 VERSION_RELEASE="" |
|
48 VERSION_PATH="" |
|
49 VERSION_REV="" |
|
50 |
|
51 while getopts "CRU:V:r:u" OPT |
|
52 do |
|
53 case "$OPT" in |
|
54 C) |
|
55 CLEAN="--clean" |
|
56 ;; |
|
57 R) |
|
58 VERSION="true" |
|
59 VERSION_RELEASE="true" |
|
60 VERSION_PATH="" |
|
61 VERSION_REV="" |
|
62 ;; |
|
63 U) |
|
64 ISABELLE_REPOS="$OPTARG" |
|
65 ;; |
|
66 V) |
|
67 VERSION="true" |
|
68 VERSION_RELEASE="" |
|
69 VERSION_PATH="$OPTARG" |
|
70 VERSION_REV="" |
|
71 ;; |
|
72 r) |
|
73 VERSION="true" |
|
74 VERSION_RELEASE="" |
|
75 VERSION_PATH="" |
|
76 VERSION_REV="$OPTARG" |
|
77 ;; |
|
78 u) |
|
79 VERSION="true" |
|
80 VERSION_RELEASE="" |
|
81 VERSION_PATH="" |
|
82 VERSION_REV="tip" |
|
83 ;; |
|
84 \?) |
|
85 usage |
|
86 ;; |
|
87 esac |
|
88 done |
|
89 |
|
90 shift $(($OPTIND - 1)) |
|
91 |
|
92 |
|
93 # args |
|
94 |
|
95 [ "$#" -ne 0 ] && usage |
|
96 |
|
97 |
|
98 ## main |
|
99 |
|
100 if [ -z "$VERSION" ]; then |
|
101 isabelle components -I && isabelle components -a |
|
102 elif [ ! -d "$ISABELLE_HOME/.hg" ]; then |
|
103 fail "Not a repository clone: cannot specify version" |
|
104 else |
|
105 if [ -n "$VERSION_REV" ]; then |
|
106 REV="$VERSION_REV" |
|
107 elif [ -n "$VERSION_RELEASE" ]; then |
|
108 URL="$ISABELLE_REPOS/raw-file/tip/Admin/Release/official" |
|
109 REV="$(curl -s -f "$URL" | head -n1)" |
|
110 [ -z "$REV" ] && fail "Failed to access \"$URL\"" |
|
111 elif [ -f "$VERSION_PATH" ]; then |
|
112 REV="$(cat "$VERSION_PATH")" |
|
113 elif [ -d "$VERSION_PATH" ]; then |
|
114 if [ -f "$VERSION_PATH/ISABELLE_VERSION" ]; then |
|
115 REV="$(cat "$VERSION_PATH/ISABELLE_VERSION")" |
|
116 else |
|
117 fail "Missing file \"$VERSION_PATH/ISABELLE_VERSION\"" |
|
118 fi |
|
119 else |
|
120 fail "Missing file \"$VERSION_PATH\"" |
|
121 fi |
|
122 |
|
123 export LANG=C |
|
124 export HGPLAIN= |
|
125 |
|
126 isabelle components -I || exit "$?" |
|
127 |
|
128 #Atomic exec: avoid inplace update of running script! |
|
129 export CLEAN REV ISABELLE_REPOS |
|
130 exec bash -c ' |
|
131 set -e |
|
132 "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS" |
|
133 "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN |
|
134 env ISABELLE_SETTINGS_PRESENT="" \ |
|
135 ISABELLE_SITE_SETTINGS_PRESENT="" \ |
|
136 ISABELLE_COMPONENTS="" \ |
|
137 ISABELLE_COMPONENTS_MISSING="" \ |
|
138 isabelle components -a |
|
139 "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV" |
|
140 if [ ! -f "$ISABELLE_HOME/lib/Tools/setup" ]; then |
|
141 echo >&2 "### The isabelle setup tool has disappeared in this version" |
|
142 echo >&2 "### (need to invoke \"${HG:-hg} update\" before using it again)" |
|
143 fi |
|
144 ' |
|
145 fi |
|