author | wenzelm |
Thu, 18 Oct 2001 21:01:18 +0200 | |
changeset 11826 | 2203c7f9ec40 |
parent 11392 | 3078f52ee552 |
child 11981 | ad67e8d2c75f |
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 |
|
10533 | 12 |
case $(hostname) in |
10532 | 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 |
{ |
|
39 |
cat <<EOF |
|
11062 | 40 |
|
41 |
Usage: $PRG VERSION |
|
42 |
||
2667 | 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 |
||
11062 | 52 |
* Check Admin/page contents. |
53 |
* Check ANNOUNCE, README, INSTALL, NEWS. |
|
54 |
* Try "isatool makeall all" with Poly/ML, SML/NJ, etc. |
|
2667 | 55 |
* Tag the current repository version, e.g.: |
10169 | 56 |
cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle99-X isabelle |
11062 | 57 |
PLEASE DO NOT DO THIS UNLESS YOU KNOW WHAT YOU ARE DOING! |
5727 | 58 |
|
2667 | 59 |
EOF |
60 |
exit 1 |
|
61 |
} |
|
62 |
||
63 |
function fail() |
|
64 |
{ |
|
65 |
echo "$1" >&2 |
|
66 |
exit 2 |
|
67 |
} |
|
68 |
||
69 |
||
70 |
## process command line |
|
71 |
||
9797 | 72 |
[ "$#" -ne 1 ] && usage |
2667 | 73 |
|
74 |
VERSION="$1" |
|
75 |
shift |
|
76 |
||
77 |
||
78 |
## main |
|
79 |
||
80 |
# dist version |
|
81 |
||
82 |
DATE=$(date "+%d-%b-%Y") |
|
4979 | 83 |
DISTDATE=$(date "+%B %Y") |
2667 | 84 |
|
9797 | 85 |
if [ "$VERSION" = "--" ]; then |
9925 | 86 |
DISTNAME="Isabelle_$DATE" |
4982 | 87 |
DISTVERSION="$DISTNAME" |
9797 | 88 |
EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME" |
9925 | 89 |
UNOFFICIAL="unofficial test" |
9797 | 90 |
elif [ "$VERSION" = "-" ]; then |
91 |
DISTNAME="Isabelle_$DATE" |
|
92 |
DISTVERSION="$DISTNAME" |
|
93 |
EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" |
|
9925 | 94 |
UNOFFICIAL="unofficial" |
2667 | 95 |
else |
96 |
DISTNAME="$VERSION" |
|
4982 | 97 |
DISTVERSION="$DISTNAME: $DISTDATE" |
9797 | 98 |
EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle" |
2667 | 99 |
UNOFFICIAL="" |
100 |
fi |
|
101 |
||
9797 | 102 |
DISTBASE="$DISTPREFIX/dist-$DISTNAME" |
103 |
mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!" |
|
104 |
[ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!" |
|
105 |
[ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!" |
|
2667 | 106 |
|
107 |
||
9797 | 108 |
# export repository |
2667 | 109 |
|
9797 | 110 |
echo "###" |
111 |
echo "### Exporting $DISTNAME ..." |
|
112 |
echo "###" |
|
2667 | 113 |
|
9797 | 114 |
cd "$DISTBASE" |
2667 | 115 |
|
9797 | 116 |
$EXPORT |
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
117 |
$FIND . -name CVS -print | xargs rm -rf |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
118 |
$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
119 |
$FIND . "(" -type d -a -empty ")" -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 |
2667 | 121 |
|
122 |
||
9797 | 123 |
# build docs |
2667 | 124 |
|
9797 | 125 |
echo "###" |
126 |
echo "### Building docs ..." |
|
127 |
echo "###" |
|
128 |
||
129 |
cd "$DISTBASE/$DISTNAME/Doc" |
|
6630 | 130 |
PDFLATEX=$(type -path pdflatex) |
3169 | 131 |
|
132 |
for DOC in $(cat Contents) |
|
2667 | 133 |
do |
9797 | 134 |
cd "$DOC" |
9925 | 135 |
make dvi |
136 |
[ -n "$PDFLATEX" ] && make clean pdf |
|
3169 | 137 |
cd .. |
2667 | 138 |
done |
139 |
||
9052 | 140 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
141 |
# prepare dist dir for release |
8059 | 142 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
143 |
echo "###" |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
144 |
echo "### Preparing distribution ..." |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
145 |
echo "###" |
2667 | 146 |
|
9797 | 147 |
cd "$DISTBASE/$DISTNAME" |
2667 | 148 |
|
9925 | 149 |
cp -R Admin/page .. |
150 |
cp Distribution/doc/Contents ../page |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
151 |
cp Distribution/lib/logo/isabelle.gif ../page/main-content |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
152 |
cp Distribution/lib/logo/isabelle.gif ../page/dist-content |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
153 |
echo "$DISTNAME" > ../page/DISTNAME |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
154 |
|
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
9880
diff
changeset
|
155 |
MOVE=$($FIND Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |
6630 | 156 |
mv -f $MOVE Distribution/doc |
3305 | 157 |
rm Distribution/doc/Isa-logics.eps |
9052 | 158 |
rm -rf Doc Tools |
2667 | 159 |
|
7115 | 160 |
mkdir src contrib |
2667 | 161 |
mv $LOGICS src |
162 |
||
163 |
mv Distribution/* . |
|
164 |
rmdir Distribution |
|
165 |
||
4180 | 166 |
( cd lib/browser; make; ) |
3638 | 167 |
|
5385 | 168 |
cp doc/isabelle*.eps lib/logo |
169 |
||
3638 | 170 |
|
2667 | 171 |
if [ -n "$UNOFFICIAL" ]; then |