author | wenzelm |
Thu, 28 Sep 2000 19:10:19 +0200 | |
changeset 10112 | 76d029a4c42e |
parent 10096 | 6cbe69107c18 |
child 10169 | dd25f5f9641a |
permissions | -rwxr-xr-x |
3060 | 1 |
#!/bin/bash |
2667 | 2 |
# |
3 |
# $Id$ |
|
4 |
# |
|
10077 | 5 |
# makedist -- make Isabelle source distribution. |
2667 | 6 |
|
7 |
||
8 |
## global settings |
|
9 |
||
7993 | 10 |
LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL ZF" |
2667 | 11 |
|
9797 | 12 |
export CVSROOT=/usr/proj/isabelle-repository/archive |
9052 | 13 |
DISTPREFIX=~/tmp/isadist |
2667 | 14 |
|
9797 | 15 |
umask 022 |
16 |
||
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
17 |
TAR=tar |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
18 |
type -path gtar >/dev/null && TAR=gtar |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
19 |
|
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
20 |
FIND=find |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
21 |
type -path gfind >/dev/null && FIND=gfind |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
22 |
|
2667 | 23 |
|
24 |
## diagnostics |
|
25 |
||
9797 | 26 |
PRG=$(basename "$0") |
27 |
THIS=$(cd $(dirname "$0"); echo "$PWD") |
|
2667 | 28 |
|
29 |
function usage() |
|
30 |
{ |
|
9797 | 31 |
echo "###" |
32 |
echo "### Usage: $PRG VERSION" |
|
33 |
echo "###" |
|
2667 | 34 |
cat <<EOF |
35 |
Make Isabelle distribution from the master sources at TUM. |
|
36 |
||
9797 | 37 |
VERSION may be either a tag like "Isabelle99-XX" that specifies the |
2667 | 38 |
release to be exported from the repository, or "-" to checkout the |
9797 | 39 |
current sources as an unofficial release, or "--" to produce a |
40 |
tentative release from the present copy of the Isabelle repository. |
|
2667 | 41 |
|
42 |
Checklist for official releases (before running this script): |
|
43 |
||
5817 | 44 |
* Check release name and date in NEWS! |
2668 | 45 |
* Check that README files are up to date (should have Id: lines). |
5769 | 46 |
* Check Admin/index.html. |
2667 | 47 |
EOF |
48 |
#Wicked! We just won't tell other users ... |
|
7859 | 49 |
if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm -o $LOGNAME = berghofe ]; then |
2667 | 50 |
cat <<EOF |
51 |
* Tag the current repository version, e.g.: |
|
9797 | 52 |
cvs -d $CVSROOT rtag Isabelle99-XX isabelle |
2667 | 53 |
PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING! |
54 |
EOF |
|
55 |
fi |
|
56 |
cat <<EOF |
|
57 |
||
58 |
After the distribution has been created succesfully, you might want |
|
59 |
to run some makeall tests using different ML systems. |
|
5727 | 60 |
|
2667 | 61 |
EOF |
62 |
exit 1 |
|
63 |
} |
|
64 |
||
65 |
function fail() |
|
66 |
{ |
|
67 |
echo "$1" >&2 |
|
68 |
exit 2 |
|
69 |
} |
|
70 |
||
71 |
||
72 |
## process command line |
|
73 |
||
9797 | 74 |
[ "$#" -ne 1 ] && usage |
2667 | 75 |
|
76 |
VERSION="$1" |
|
77 |
shift |
|
78 |
||
79 |
||
80 |
## main |
|
81 |
||
82 |
# dist version |
|
83 |
||
84 |
DATE=$(date "+%d-%b-%Y") |
|
4979 | 85 |
DISTDATE=$(date "+%B %Y") |
2667 | 86 |
|
9797 | 87 |
if [ "$VERSION" = "--" ]; then |
9925 | 88 |
DISTNAME="Isabelle_$DATE" |
4982 | 89 |
DISTVERSION="$DISTNAME" |
9797 | 90 |
EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME" |
9925 | 91 |
UNOFFICIAL="unofficial test" |
9797 | 92 |
elif [ "$VERSION" = "-" ]; then |
93 |
DISTNAME="Isabelle_$DATE" |
|
94 |
DISTVERSION="$DISTNAME" |
|
95 |
EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" |
|
9925 | 96 |
UNOFFICIAL="unofficial" |
2667 | 97 |
else |
98 |
DISTNAME="$VERSION" |
|
4982 | 99 |
DISTVERSION="$DISTNAME: $DISTDATE" |
9797 | 100 |
EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle" |
2667 | 101 |
UNOFFICIAL="" |
102 |
fi |
|
103 |
||
9797 | 104 |
DISTBASE="$DISTPREFIX/dist-$DISTNAME" |
105 |
mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!" |
|
106 |
[ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!" |
|
107 |
[ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!" |
|
2667 | 108 |
|
109 |
||
9797 | 110 |
# export repository |
2667 | 111 |
|
9797 | 112 |
echo "###" |
113 |
echo "### Exporting $DISTNAME ..." |
|
114 |
echo "###" |
|
2667 | 115 |
|
9797 | 116 |
cd "$DISTBASE" |
2667 | 117 |
|
9797 | 118 |
$EXPORT |
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
119 |
$FIND . -name CVS -print | xargs rm -rf |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
120 |
$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
121 |
$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
122 |
$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf |
2667 | 123 |
|
124 |
||
9797 | 125 |
# build docs |
2667 | 126 |
|
9797 | 127 |
echo "###" |
128 |
echo "### Building docs ..." |
|
129 |
echo "###" |
|
130 |
||
131 |
cd "$DISTBASE/$DISTNAME/Doc" |
|
6630 | 132 |
PDFLATEX=$(type -path pdflatex) |
3169 | 133 |
|
134 |
for DOC in $(cat Contents) |
|
2667 | 135 |
do |
9797 | 136 |
cd "$DOC" |
9925 | 137 |
make dvi |
138 |
[ -n "$PDFLATEX" ] && make clean pdf |
|
3169 | 139 |
cd .. |
2667 | 140 |
done |
141 |
||
9052 | 142 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
143 |
# prepare dist dir for release |
8059 | 144 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
145 |
echo "###" |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
146 |
echo "### Preparing distribution ..." |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
147 |
echo "###" |
2667 | 148 |
|
9797 | 149 |
cd "$DISTBASE/$DISTNAME" |
2667 | 150 |
|
9925 | 151 |
cp -R Admin/page .. |
152 |
cp Distribution/doc/Contents ../page |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
153 |
cp Distribution/lib/logo/isabelle.gif ../page/main-content |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
154 |
cp Distribution/lib/logo/isabelle.gif ../page/dist-content |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
155 |
echo "$DISTNAME" > ../page/DISTNAME |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
156 |
|
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
157 |
MOVE=$($FIND Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |
6630 | 158 |
mv -f $MOVE Distribution/doc |
3305 | 159 |
rm Distribution/doc/Isa-logics.eps |
9052 | 160 |
rm -rf Doc Tools |
2667 | 161 |
|
7115 | 162 |
mkdir src contrib |
2667 | 163 |
mv $LOGICS src |
164 |
||
165 |
mv Distribution/* . |
|
166 |
rmdir Distribution |
|
167 |
||
4180 | 168 |
( cd lib/browser; make; ) |
3638 | 169 |
|
5385 | 170 |
cp doc/isabelle*.eps lib/logo |
171 |
||
3638 | 172 |
|
2667 | 173 |
if [ -n "$UNOFFICIAL" ]; then |
174 |
{ |
|
175 |
echo |
|
176 |
echo "IMPORTANT NOTE" |
|
177 |
echo "==============" |
|
178 |
echo |
|
9925 | 179 |
echo "This is an $UNOFFICIAL release of Isabelle, created by $LOGNAME $DATE." |
2667 | 180 |
echo |
9925 | 181 |
} >ANNOUNCE |
2667 | 182 |
fi |
183 |
||
8810 | 184 |
perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html |
9959 | 185 |
perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML |
4986 | 186 |
perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html |
3257 | 187 |
lynx -dump README.html >README |
188 |
||
9052 | 189 |
( cd src; ../Admin/maketags; ) |
10077 | 190 |
|
191 |
( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure ) |
|
192 |
||
9052 | 193 |
rm -rf Admin |
194 |
||
2667 | 195 |
|
196 |
# create archive |
|
197 |
||
9797 | 198 |
echo "###" |
199 |
echo "### Creating archives ..." |
|
200 |
echo "###" |
|
2667 | 201 |
|
9797 | 202 |
cd "$DISTBASE" |
203 |
||
10087 | 204 |
echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST |
205 |
||
10068 | 206 |
rm -f Isabelle |
207 |
ln -s "$DISTNAME" Isabelle |
|
208 |
||
9797 | 209 |
chown -R "$LOGNAME" "$DISTNAME" |
210 |
chmod -R u+w "$DISTNAME" |
|
211 |
chmod -R g=o "$DISTNAME" |
|
10077 | 212 |
chgrp -R isabelle "$DISTNAME" Isabelle |
2667 | 213 |
|
9797 | 214 |
mkdir -p "pdf/$DISTNAME/doc" |
215 |
mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" |
|
6748 | 216 |
|
10096 | 217 |
echo "$DISTNAME.tar.gz" |
10077 | 218 |
"$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" |
10096 | 219 |
gzip "$DISTNAME.tar" |
220 |
||
221 |
echo "${DISTNAME}_pdf.tar.gz" |
|
10112 | 222 |
( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) |
10096 | 223 |
gzip "${DISTNAME}_pdf.tar" |
6748 | 224 |
|
9797 | 225 |
mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" |
226 |
rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf |
|
6750 | 227 |
|
6304 | 228 |
|
9782 | 229 |
# cleanup dist |
230 |
||
9797 | 231 |
mv "$DISTNAME" "${DISTNAME}-old" |
232 |
mkdir "$DISTNAME" |
|
9782 | 233 |
|
10017 | 234 |
mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" "$DISTNAME" |
9797 | 235 |
mkdir "$DISTNAME/doc" |
9925 | 236 |
mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc" |
9782 | 237 |
|
9867 | 238 |
chgrp -R isabelle "$DISTNAME" |
239 |
||
9797 | 240 |
rm -rf "${DISTNAME}-old" |
9782 | 241 |
|
242 |
||
2667 | 243 |
# final note |
244 |
||
9797 | 245 |
echo "###" |
10112 | 246 |
echo "### Finished makedist." |
9797 | 247 |
echo "###" |