1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # makedist_mercurial -- make Isabelle source distribution (via Mercurial) |
|
6 |
|
7 ## global settings |
|
8 |
|
9 REPOS="http://isabelle.in.tum.de/repos/isabelle" |
|
10 |
|
11 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist} |
|
12 |
|
13 umask 022 |
|
14 |
|
15 |
|
16 ## diagnostics |
|
17 |
|
18 PRG=$(basename "$0") |
|
19 THIS=$(cd $(dirname "$0"); echo "$PWD") |
|
20 |
|
21 function usage() |
|
22 { |
|
23 cat <<EOF |
|
24 |
|
25 Usage: $PRG [OPTIONS] [VERSION] |
|
26 |
|
27 Options are: |
|
28 -r RELEASE proper release with name" |
|
29 |
|
30 Make Isabelle distribution from the main Mercurial repository at TUM. |
|
31 |
|
32 VERSION identifies the snapshot, using usual Mercurial terminology; |
|
33 the default is RELEASE if given, otherwise "tip". |
|
34 |
|
35 EOF |
|
36 exit 1 |
|
37 } |
|
38 |
|
39 function fail() |
|
40 { |
|
41 echo "$1" >&2 |
|
42 exit 2 |
|
43 } |
|
44 |
|
45 |
|
46 ## process command line |
|
47 |
|
48 # options |
|
49 |
|
50 RELEASE="" |
|
51 |
|
52 while getopts "r:" OPT |
|
53 do |
|
54 case "$OPT" in |
|
55 r) |
|
56 RELEASE="$OPTARG" |
|
57 ;; |
|
58 \?) |
|
59 usage |
|
60 ;; |
|
61 esac |
|
62 done |
|
63 |
|
64 shift $(($OPTIND - 1)) |
|
65 |
|
66 |
|
67 # args |
|
68 |
|
69 VERSION="" |
|
70 [ "$#" -gt 0 ] && { VERSION="$1"; shift; } |
|
71 [ -z "$VERSION" ] && VERSION="$RELEASE" |
|
72 [ -z "$VERSION" ] && VERSION="tip" |
|
73 |
|
74 [ "$#" -gt 0 ] && usage |
|
75 |
|
76 |
|
77 ## main |
|
78 |
|
79 # tmp |
|
80 |
|
81 TMP="tmp-$USER$$" |
|
82 function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; } |
|
83 |
|
84 |
|
85 # retrieve archive and resolve version identifier |
|
86 |
|
87 mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory" |
|
88 cd "$DISTPREFIX/$TMP" |
|
89 |
|
90 echo "###" |
|
91 echo "### Retrieving Mercurial snapshot $VERSION" |
|
92 echo "###" |
|
93 |
|
94 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \ |
|
95 fail "Failed to retrieve $VERSION" |
|
96 |
|
97 IDENT=$(echo * | sed 's/isabelle-//') |
|
98 |
|
99 rm -f "isabelle-$IDENT/.hg_archival.txt" |
|
100 rm -f "isabelle-$IDENT/.hgtags" |
|
101 rm -f "isabelle-$IDENT/.hgignore" |
|
102 rm -f "isabelle-$IDENT/README_REPOSITORY" |
|
103 |
|
104 |
|
105 # dist name |
|
106 |
|
107 DATE=$(env LC_ALL=C date "+%d-%b-%Y") |
|
108 DISTDATE=$(env LC_ALL=C date "+%B %Y") |
|
109 |
|
110 if [ -z "$RELEASE" ]; then |
|
111 DISTNAME="Isabelle_$DATE" |
|
112 DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)" |
|
113 else |
|
114 DISTNAME="$RELEASE" |
|
115 DISTVERSION="$DISTNAME: $DISTDATE" |
|
116 fi |
|
117 |
|
118 DISTBASE="$DISTPREFIX/dist-$DISTNAME" |
|
119 mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; } |
|
120 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; } |
|
121 [ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; } |
|
122 |
|
123 cd "$DISTBASE" |
|
124 mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME" |
|
125 purge_tmp |
|
126 |
|
127 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME" |
|
128 |
|
129 |
|
130 # website |
|
131 |
|
132 mkdir -p ../website |
|
133 cat > ../website/distinfo.mak <<EOF |
|
134 # this is a generated file - do not edit unless you know what you are doing! |
|
135 DISTNAME=$DISTNAME |
|
136 DISTBASE=$DISTBASE |
|
137 EOF |
|
138 |
|
139 cp lib/html/library_index_content.template ../website/ |
|
140 |
|
141 |
|
142 # prepare dist for release |
|
143 |
|
144 echo "###" |
|
145 echo "### Preparing distribution $DISTNAME" |
|
146 echo "###" |
|
147 |
|
148 find . -name .cvsignore -print | xargs rm -rf |
|
149 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x |
|
150 find . -print | xargs chmod u+rw |
|
151 |
|
152 ./Admin/build all || fail "Failed to build distribution" |
|
153 rm -rf Admin |
|
154 |
|
155 MOVE=$(find doc-src \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |
|
156 mv -f $MOVE doc |
|
157 rm doc/Isa-logics.eps |
|
158 rm doc/codegen_process.pdf |
|
159 rm -rf doc-src |
|
160 |
|
161 mkdir contrib |
|
162 |
|
163 cp doc/isabelle*.eps lib/logo |
|
164 |
|
165 |
|
166 if [ -z "$RELEASE" ]; then |
|
167 { |
|
168 echo |
|
169 echo "IMPORTANT NOTE" |
|
170 echo "==============" |
|
171 echo |
|
172 echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE." |
|
173 echo "See $REPOS/log/$IDENT for details." |
|
174 echo |
|
175 } >ANNOUNCE |
|
176 else |
|
177 perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML |
|
178 fi |
|
179 |
|
180 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML |
|
181 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings |
|
182 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template |
|
183 perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version |
|
184 perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README |
|
185 |
|
186 |
|
187 # create archives |
|
188 |
|
189 echo "###" |
|
190 echo "### Creating archives ..." |
|
191 echo "###" |
|
192 |
|
193 cd "$DISTBASE" |
|
194 |
|
195 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST |
|
196 echo "$IDENT" >../ISABELLE_IDENT |
|
197 |
|
198 rm -f Isabelle |
|
199 ln -s "$DISTNAME" Isabelle |
|
200 |
|
201 chown -R "$LOGNAME" "$DISTNAME" |
|
202 chmod -R u+w "$DISTNAME" |
|
203 chmod -R g=o "$DISTNAME" |
|
204 chgrp -R isabelle "$DISTNAME" Isabelle |
|
205 |
|
206 mkdir -p "pdf/$DISTNAME/doc" |
|
207 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" |
|
208 |
|
209 echo "$DISTNAME.tar.gz" |
|
210 tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME" |
|
211 |
|
212 echo "${DISTNAME}_pdf.tar.gz" |
|
213 tar -C pdf -czf "${DISTNAME}_pdf.tar.gz" "$DISTNAME" |
|
214 |
|
215 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" |
|
216 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf |
|
217 |
|
218 |
|
219 # cleanup dist |
|
220 |
|
221 mv "$DISTNAME" "${DISTNAME}-old" |
|
222 mkdir "$DISTNAME" |
|
223 |
|
224 mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ |
|
225 "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ |
|
226 "$DISTNAME" |
|
227 mkdir "$DISTNAME/doc" |
|
228 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" |
|
229 |
|
230 chgrp -R isabelle "$DISTNAME" |
|
231 |
|
232 rm -rf "${DISTNAME}-old" |
|
233 |
|