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