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