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