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