author | wenzelm |
Thu, 17 Jul 2008 17:10:53 +0200 | |
changeset 27637 | 47ceef8aa1e4 |
parent 27633 | c2984f0684ee |
child 27638 | ef8a96456b3c |
permissions | -rwxr-xr-x |
12721 | 1 |
#!/usr/bin/env bash |
2667 | 2 |
# |
3 |
# $Id$ |
|
4 |
# |
|
10077 | 5 |
# makedist -- make Isabelle source distribution. |
2667 | 6 |
|
7 |
||
8 |
## global settings |
|
9 |
||
17554 | 10 |
DISTPREFIX=${DISTPREFIX:-~/tmp/isadist} |
23149 | 11 |
SRCS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents Tools ZF" |
2667 | 12 |
|
26372 | 13 |
export CVSROOT=/home/isabelle-repository/archive |
26370
2a4f0d0621f1
remote CVSROOT: default to atbroy100 instead of sunbroy2;
wenzelm
parents:
26133
diff
changeset
|
14 |
[ ! -d "$CVSROOT" ] && CVSROOT="${ISABELLE_USER:-$USER}@atbroy100.informatik.tu-muenchen.de:$CVSROOT" |
2667 | 15 |
|
27633 | 16 |
[ -z "$CVS2CL" ] && type -path cvs2cl >/dev/null && CVS2CL=cvs2cl |
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
17 |
|
27633 | 18 |
umask 022 |
26370
2a4f0d0621f1
remote CVSROOT: default to atbroy100 instead of sunbroy2;
wenzelm
parents:
26133
diff
changeset
|
19 |
|
2667 | 20 |
|
21 |
## diagnostics |
|
22 |
||
9797 | 23 |
PRG=$(basename "$0") |
24 |
THIS=$(cd $(dirname "$0"); echo "$PWD") |
|
2667 | 25 |
|
26 |
function usage() |
|
27 |
{ |
|
28 |
cat <<EOF |
|
11062 | 29 |
|
17554 | 30 |
Usage: $PRG VERSION [NAME] |
11062 | 31 |
|
2667 | 32 |
Make Isabelle distribution from the master sources at TUM. |
33 |
||
17693 | 34 |
VERSION may be either a tag like "IsabelleXXXX" that specifies the |
2667 | 35 |
release to be exported from the repository, or "-" to checkout the |
17554 | 36 |
current sources as an unofficial release. |
37 |
||
38 |
NAME specifies an explicit distribution name, by default it is |
|
39 |
derived from VERSION. |
|
2667 | 40 |
EOF |
41 |
exit 1 |
|
42 |
} |
|
43 |
||
44 |
function fail() |
|
45 |
{ |
|
46 |
echo "$1" >&2 |
|
47 |
exit 2 |
|
48 |
} |
|
49 |
||
50 |
||
51 |
## process command line |
|
52 |
||
17554 | 53 |
[ "$#" -ne 1 -a "$#" -ne 2 ] && usage |
54 |
||
55 |
VERSION="$1"; shift |
|
2667 | 56 |
|
17554 | 57 |
if [ "$#" -eq 0 ]; then |
58 |
DISTNAME="" |
|
59 |
else |
|
60 |
DISTNAME="$1"; shift |
|
61 |
fi |
|
2667 | 62 |
|
63 |
||
64 |
## main |
|
65 |
||
66 |
# dist version |
|
67 |
||
21712
8b2fd895a7fc
date: forcing LC_ALL=C prevents funny file names;
wenzelm
parents:
20990
diff
changeset
|
68 |
DATE=$(env LC_ALL=C date "+%d-%b-%Y") |
8b2fd895a7fc
date: forcing LC_ALL=C prevents funny file names;
wenzelm
parents:
20990
diff
changeset
|
69 |
DISTDATE=$(env LC_ALL=C date "+%B %Y") |
2667 | 70 |
|
17554 | 71 |
if [ "$VERSION" = "-" ]; then |
72 |
DISTIDENT="Isabelle_$DATE" |
|
73 |
[ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" |
|
9797 | 74 |
DISTVERSION="$DISTNAME" |
75 |
EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" |
|
17558 | 76 |
UNOFFICIAL=true |
2667 | 77 |
else |
17554 | 78 |
DISTIDENT="$VERSION" |
79 |
[ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" |
|
4982 | 80 |
DISTVERSION="$DISTNAME: $DISTDATE" |
17561 | 81 |
EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle" |
2667 | 82 |
UNOFFICIAL="" |
83 |
fi |
|
84 |
||
9797 | 85 |
DISTBASE="$DISTPREFIX/dist-$DISTNAME" |
86 |
mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!" |
|
87 |
[ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!" |
|
88 |
[ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!" |
|
2667 | 89 |
|
90 |
||
9797 | 91 |
# export repository |
2667 | 92 |
|
9797 | 93 |
echo "###" |
17554 | 94 |
echo "### Exporting $DISTIDENT ..." |
9797 | 95 |
echo "###" |
2667 | 96 |
|
9797 | 97 |
cd "$DISTBASE" |
2667 | 98 |
|
13230
c5fad3c40d45
fail more gracefully, return proper exit codes, allow preset DISTPREFIX
kleing
parents:
13100
diff
changeset
|
99 |
$EXPORT || fail "Export failed!" |
15438 | 100 |
|
27029 | 101 |
if [ -n "$CVS2CL" -a -n "$UNOFFICIAL" ]; then |
15438 | 102 |
cd $DISTNAME |
103 |
$CVS2CL |
|
104 |
gzip ChangeLog |
|
26108 | 105 |
cp ChangeLog.gz .. |
15438 | 106 |
cd .. |
107 |
fi |
|
108 |
||
27633 | 109 |
find . -name CVS -print | xargs rm -rf |
110 |
find . -name .cvsignore -print | xargs rm -rf |
|
111 |
find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x |
|
112 |
find . -print | xargs chmod u+rw |
|
2667 | 113 |
|
114 |
||
27633 | 115 |
# build components |
9797 | 116 |
|
27633 | 117 |
"$DISTBASE/$DISTNAME/Admin/build" all || fail "Failed to build distribution" |
2667 | 118 |
|
9052 | 119 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
120 |
# prepare dist dir for release |
8059 | 121 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
122 |
echo "###" |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
123 |
echo "### Preparing distribution ..." |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
124 |
echo "###" |
2667 | 125 |
|
17554 | 126 |
cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME" |
2667 | 127 |
|
25237 | 128 |
mkdir -p ../website |
129 |
cat > ../website/distinfo.mak <<EOF |
|
17942
68988fd2fd27
towards an improved website/makedist integration
haftmann
parents:
17910
diff
changeset
|
130 |
# this is a generated file - do not edit unless you know what you are doing! |
16301 | 131 |
|
132 |
DISTNAME=$DISTNAME |
|
17554 | 133 |
DISTIDENT=$DISTIDENT |
17910 | 134 |
DISTBASE=$DISTBASE |
16301 | 135 |
EOF |
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
136 |
|
25237 | 137 |
cp Distribution/lib/html/library_index_content.template ../website/ |
138 |
||
27633 | 139 |
MOVE=$(find Doc \( -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') |
6630 | 140 |
mv -f $MOVE Distribution/doc |
3305 | 141 |
rm Distribution/doc/Isa-logics.eps |
27090 | 142 |
rm Distribution/doc/codegen_process.pdf |
23201 | 143 |
rm -rf Doc |
2667 | 144 |
|
7115 | 145 |
mkdir src contrib |
23149 | 146 |
mv $SRCS src |
2667 | 147 |
|
148 |
mv Distribution/* . |
|
149 |
rmdir Distribution |
|
150 |
||
25949
850b4c2d0f17
reactivated mk of java/scala sources, with paranoia PATH setting for sunbroy;
wenzelm
parents:
25859
diff
changeset
|
151 |
|
5385 | 152 |
cp doc/isabelle*.eps lib/logo |
153 |
||
3638 | 154 |
|
2667 | 155 |
if [ -n "$UNOFFICIAL" ]; then |
156 |
{ |
|
157 |
echo |
|
158 |
echo "IMPORTANT NOTE" |
|
159 |
echo "==============" |
|
160 |
echo |
|
17554 | 161 |
echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE." |
2667 | 162 |
echo |
9925 | 163 |
} >ANNOUNCE |
26133 | 164 |
perl -pi -e "s/val is_official = true/val is_official = false/" src/Pure/ROOT.ML |
2667 | 165 |
fi |
166 |
||
25433 | 167 |
perl -pi -e "s/ISABELLE_IDENTIFIER=\"\"/ISABELLE_IDENTIFIER=\"$DISTNAME\"/g;" lib/scripts/getsettings |
25237 | 168 |
perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/library_index_header.template |
17554 | 169 |
perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version |
25214 | 170 |
perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README |
3257 | 171 |
|
10077 | 172 |
|
9052 | 173 |
rm -rf Admin |
174 |
||
2667 | 175 |
|
176 |
# create archive |
|
177 |
||
9797 | 178 |
echo "###" |
179 |
echo "### Creating archives ..." |
|
180 |
echo "###" |
|
2667 | 181 |
|
9797 | 182 |
cd "$DISTBASE" |
183 |
||
10087 | 184 |
echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST |
185 |
||
10068 | 186 |
rm -f Isabelle |
187 |
ln -s "$DISTNAME" Isabelle |
|
188 |
||
9797 | 189 |
chown -R "$LOGNAME" "$DISTNAME" |
190 |
chmod -R u+w "$DISTNAME" |
|
191 |
chmod -R g=o "$DISTNAME" |
|
10077 | 192 |
chgrp -R isabelle "$DISTNAME" Isabelle |
2667 | 193 |
|
9797 | 194 |
mkdir -p "pdf/$DISTNAME/doc" |
17655 | 195 |
mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" |
196 |
||
197 |
sync; sleep 3 |
|
6748 | 198 |
|
10096 | 199 |
echo "$DISTNAME.tar.gz" |
27633 | 200 |
tar cf "$DISTNAME.tar" Isabelle "$DISTNAME" |
10096 | 201 |
gzip "$DISTNAME.tar" |
202 |
||
203 |
echo "${DISTNAME}_pdf.tar.gz" |
|
27633 | 204 |
( cd pdf; tar cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) |
10096 | 205 |
gzip "${DISTNAME}_pdf.tar" |
6748 | 206 |
|
17655 | 207 |
mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" |
9797 | 208 |
rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf |
6750 | 209 |
|
6304 | 210 |
|
9782 | 211 |
# cleanup dist |
212 |
||
9797 | 213 |
mv "$DISTNAME" "${DISTNAME}-old" |
214 |
mkdir "$DISTNAME" |
|
9782 | 215 |
|
25214 | 216 |
mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ |
17554 | 217 |
"${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ |
218 |
"$DISTNAME" |
|
9797 | 219 |
mkdir "$DISTNAME/doc" |
17655 | 220 |
mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" |
9782 | 221 |
|
9867 | 222 |
chgrp -R isabelle "$DISTNAME" |
223 |
||
9797 | 224 |
rm -rf "${DISTNAME}-old" |
9782 | 225 |
|
226 |
||
2667 | 227 |
# final note |
228 |
||
9797 | 229 |
echo "###" |
10112 | 230 |
echo "### Finished makedist." |
9797 | 231 |
echo "###" |