27644
|
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/isabelle-bin/mercurial.cgi"
|
|
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 NAME proper release with name"
|
|
29 |
|
27645
|
30 |
Make Isabelle distribution from the Mercurial repository at TUM.
|
27644
|
31 |
|
27645
|
32 |
VERSION identifies the snapshot, using usual Mercurial terminology;
|
|
33 |
the default is "tip", or the proper release name if given.
|
27644
|
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 |
|
27645
|
69 |
VERSION=""
|
27644
|
70 |
[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
|
|
71 |
|
|
72 |
[ "$#" -gt 0 ] && usage
|
|
73 |
|
|
74 |
|
27645
|
75 |
# defaults
|
|
76 |
|
|
77 |
if [ -z "$RELEASE" ]; then
|
|
78 |
[ -z "$VERSION" ] && VERSION=tip
|
|
79 |
else
|
|
80 |
[ -z "$VERSION" ] && VERSION="$RELEASE"
|
|
81 |
fi
|
|
82 |
|
|
83 |
|
27644
|
84 |
## main
|
|
85 |
|
27648
|
86 |
# tmp
|
|
87 |
|
|
88 |
TMP="tmp-$USER$$"
|
|
89 |
function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
|
|
90 |
|
|
91 |
|
27644
|
92 |
# retrieve archive and resolve version identifier
|
|
93 |
|
|
94 |
mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
|
|
95 |
cd "$DISTPREFIX/$TMP"
|
|
96 |
|
|
97 |
echo "###"
|
27645
|
98 |
echo "### Retrieving Mercurial snapshot ${VERSION}.tar.gz"
|
27644
|
99 |
echo "###"
|
|
100 |
|
|
101 |
{ wget -q "$REPOS/archive/${VERSION}.tar.gz" && tar -x -z -f "${VERSION}.tar.gz"; } || \
|
|
102 |
fail "Failed to retrieve $VERSION"
|
|
103 |
|
|
104 |
rm "${VERSION}.tar.gz"
|
|
105 |
IDENT=$(echo * | sed 's/Isabelle-repository-//')
|
|
106 |
|
27645
|
107 |
rm -f "Isabelle-repository-$IDENT/.hg_archival.txt"
|
|
108 |
rm -f "Isabelle-repository-$IDENT/.hgtags"
|
27644
|
109 |
|
|
110 |
|
|
111 |
# dist name
|
|
112 |
|
|
113 |
DATE=$(env LC_ALL=C date "+%d-%b-%Y")
|
|
114 |
DISTDATE=$(env LC_ALL=C date "+%B %Y")
|
|
115 |
|
|
116 |
if [ -z "$RELEASE" ]; then
|
|
117 |
DISTNAME="Isabelle_$DATE"
|
|
118 |
DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
|
|
119 |
else
|
|
120 |
DISTNAME="$RELEASE"
|
|
121 |
DISTVERSION="$DISTNAME: $DISTDATE"
|
|
122 |
fi
|
|
123 |
|
|
124 |
DISTBASE="$DISTPREFIX/dist-$DISTNAME"
|
27648
|
125 |
mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
|
|
126 |
[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
|
|
127 |
[ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
|
27644
|
128 |
|
|
129 |
cd "$DISTBASE"
|
|
130 |
mv "$DISTPREFIX/$TMP/Isabelle-repository-$IDENT" "$DISTNAME"
|
27648
|
131 |
purge_tmp
|
27644
|
132 |
|
|
133 |
cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
|
|
134 |
|
|
135 |
|
|
136 |
# website
|
|
137 |
|
|
138 |
mkdir -p ../website
|
|
139 |
cat > ../website/distinfo.mak <<EOF
|
|
140 |
# this is a generated file - do not edit unless you know what you are doing!
|
|
141 |
|
|
142 |
DISTNAME=$DISTNAME
|
|
143 |
DISTBASE=$DISTBASE
|
|
144 |
EOF
|
|
145 |
|
|
146 |
cp lib/html/library_index_content.template ../website/
|
|
147 |
|
|
148 |
|
|
149 |
# prepare dist for release
|
|
150 |
|
|
151 |
echo "###"
|
|
152 |
echo "### Preparing distribution $DISTNAME"
|
|
153 |
echo "###"
|
|
154 |
|
27648
|
155 |
find . -name .cvsignore -print | xargs rm -rf
|
27644
|
156 |
find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
|
|
157 |
find . -print | xargs chmod u+rw
|
|
158 |
|
|
159 |
./Admin/build all || fail "Failed to build distribution"
|
|
160 |
rm -rf Admin
|
|
161 |
|
|
162 |
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')
|
|
163 |
mv -f $MOVE doc
|
|
164 |
rm doc/Isa-logics.eps
|
|
165 |
rm doc/codegen_process.pdf
|
|
166 |
rm -rf doc-src
|
|
167 |
|
|
168 |
mkdir contrib
|
|
169 |
|
|
170 |
cp doc/isabelle*.eps lib/logo
|
|
171 |
|
|
172 |
|
|
173 |
if [ -z "$RELEASE" ]; then
|
|
174 |
{
|
|
175 |
echo
|
|
176 |
echo "IMPORTANT NOTE"
|
|
177 |
echo "=============="
|
|
178 |
echo
|
|
179 |
echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
|
|
180 |
echo "See $REPOS/log/$IDENT for details."
|
|
181 |
echo
|
|
182 |
} >ANNOUNCE
|
|
183 |
else
|
27645
|
184 |
perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
|
27644
|
185 |
fi
|
|
186 |
|
27645
|
187 |
perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
|
|
188 |
perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
|
|
189 |
perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
|
|
190 |
perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
|
|
191 |
perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README
|
27644
|
192 |
|
|
193 |
|
|
194 |
# create archives
|
|
195 |
|
|
196 |
echo "###"
|
|
197 |
echo "### Creating archives ..."
|
|
198 |
echo "###"
|
|
199 |
|
|
200 |
cd "$DISTBASE"
|
|
201 |
|
|
202 |
echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
|
|
203 |
echo "$IDENT" >../ISABELLE_IDENT
|
|
204 |
|
|
205 |
rm -f Isabelle
|
|
206 |
ln -s "$DISTNAME" Isabelle
|
|
207 |
|
|
208 |
chown -R "$LOGNAME" "$DISTNAME"
|
|
209 |
chmod -R u+w "$DISTNAME"
|
|
210 |
chmod -R g=o "$DISTNAME"
|
|
211 |
chgrp -R isabelle "$DISTNAME" Isabelle
|
|
212 |
|
|
213 |
mkdir -p "pdf/$DISTNAME/doc"
|
|
214 |
mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
|
|
215 |
|
|
216 |
echo "$DISTNAME.tar.gz"
|
|
217 |
tar -c -z -f "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
|
|
218 |
|
|
219 |
echo "${DISTNAME}_pdf.tar.gz"
|
|
220 |
tar -C pdf -c -z -f "${DISTNAME}_pdf.tar.gz" "$DISTNAME"
|
|
221 |
|
|
222 |
mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
|
|
223 |
rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
|
|
224 |
|
|
225 |
|
|
226 |
# cleanup dist
|
|
227 |
|
|
228 |
mv "$DISTNAME" "${DISTNAME}-old"
|
|
229 |
mkdir "$DISTNAME"
|
|
230 |
|
|
231 |
mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
|
|
232 |
"${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
|
|
233 |
"$DISTNAME"
|
|
234 |
mkdir "$DISTNAME/doc"
|
|
235 |
mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
|
|
236 |
|
|
237 |
chgrp -R isabelle "$DISTNAME"
|
|
238 |
|
|
239 |
rm -rf "${DISTNAME}-old"
|
|
240 |
|
|
241 |
echo "###"
|
|
242 |
echo "### Finished makedist."
|
|
243 |
echo "###"
|