2667
|
1 |
#!/bin/bash -norc
|
|
2 |
#
|
|
3 |
# $Id$
|
|
4 |
#
|
|
5 |
# makedist -- make Isabelle distribution.
|
|
6 |
|
|
7 |
|
|
8 |
## global settings
|
|
9 |
|
|
10 |
LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF LK Modal Provers Pure Sequents TFL Tools ZF"
|
|
11 |
DOCS="Intro Ref Logics"
|
|
12 |
|
|
13 |
CVSROOT=/isabelle/archive
|
|
14 |
DISTBASE=~/tmp/isadist
|
|
15 |
|
|
16 |
|
|
17 |
## diagnostics
|
|
18 |
|
|
19 |
PRG=$(basename $0)
|
|
20 |
|
|
21 |
function usage()
|
|
22 |
{
|
|
23 |
echo
|
|
24 |
echo "Usage: $PRG VERSION"
|
|
25 |
echo
|
|
26 |
cat <<EOF
|
|
27 |
Make Isabelle distribution from the master sources at TUM.
|
|
28 |
|
|
29 |
VERSION may be either a tag like "Isabelle94-XX" that specifies the
|
|
30 |
release to be exported from the repository, or "-" to checkout the
|
|
31 |
current sources as an unofficial release.
|
|
32 |
|
|
33 |
Checklist for official releases (before running this script):
|
|
34 |
|
2668
|
35 |
* Check that README files are up to date (should have Id: lines).
|
2667
|
36 |
* Check that Pure/ROOT.ML/version is up to date!
|
2686
|
37 |
* Check release name and date in NEWS!
|
2667
|
38 |
* Make sure that the repository version of Doc is consistent
|
|
39 |
(watch out for *.bbl, *.rao, *.ind)!
|
|
40 |
EOF
|
|
41 |
#Wicked! We just won't tell other users ...
|
|
42 |
if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then
|
|
43 |
cat <<EOF
|
|
44 |
* Tag the current repository version, e.g.:
|
|
45 |
cvs rtag Isabelle94-XX isabelle
|
|
46 |
PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
|
|
47 |
EOF
|
|
48 |
fi
|
|
49 |
cat <<EOF
|
|
50 |
|
|
51 |
After the distribution has been created succesfully, you might want
|
|
52 |
to run some makeall tests using different ML systems.
|
|
53 |
|
|
54 |
EOF
|
|
55 |
exit 1
|
|
56 |
}
|
|
57 |
|
|
58 |
function fail()
|
|
59 |
{
|
|
60 |
echo "$1" >&2
|
|
61 |
exit 2
|
|
62 |
}
|
|
63 |
|
|
64 |
|
|
65 |
## process command line
|
|
66 |
|
|
67 |
[ $# -ne 1 ] && usage
|
|
68 |
|
|
69 |
VERSION="$1"
|
|
70 |
shift
|
|
71 |
|
|
72 |
|
|
73 |
## main
|
|
74 |
|
|
75 |
# dist version
|
|
76 |
|
|
77 |
DATE=$(date "+%d-%b-%Y")
|
|
78 |
|
|
79 |
if [ "$VERSION" = "-" ]; then
|
|
80 |
DISTNAME=Isabelle_$DATE
|
|
81 |
EXPORT="checkout"
|
|
82 |
UNOFFICIAL=true
|
|
83 |
else
|
|
84 |
DISTNAME="$VERSION"
|
|
85 |
EXPORT="export -r $VERSION"
|
|
86 |
UNOFFICIAL=""
|
|
87 |
fi
|
|
88 |
|
|
89 |
mkdir -p $DISTBASE || fail "Unable to create distribution base dir $DISTBASE!"
|
|
90 |
[ -e $DISTBASE/$DISTNAME ] && fail "$DISTBASE/$DISTNAME already exists!"
|
|
91 |
|
|
92 |
|
|
93 |
# export from repository
|
|
94 |
|
|
95 |
echo
|
|
96 |
echo "Exporting $DISTNAME from repository. Please be patient ..."
|
|
97 |
echo
|
|
98 |
|
|
99 |
cd $DISTBASE
|
|
100 |
|
|
101 |
export CVSROOT
|
|
102 |
cvs -f -q $EXPORT -d $DISTNAME isabelle
|
|
103 |
|
|
104 |
|
|
105 |
# make docs
|
|
106 |
|
|
107 |
for D in $DOCS
|
|
108 |
do
|
|
109 |
cd $DISTBASE/$DISTNAME/Doc/$D
|
|
110 |
make dist
|
|
111 |
done
|
|
112 |
|
|
113 |
|
|
114 |
# prepare dist dir for release
|
|
115 |
|
|
116 |
cd $DISTBASE/$DISTNAME
|
|
117 |
|
|
118 |
find . -name CVS -exec rm -rf {} \;
|
|
119 |
|
|
120 |
find Doc -name \*.dvi -exec mv {} Distribution/doc \;
|
|
121 |
rm -rf Admin Doc examples index.html
|
|
122 |
|
|
123 |
mkdir src
|
|
124 |
mv $LOGICS src
|
|
125 |
|
|
126 |
mv Distribution/* .
|
|
127 |
rmdir Distribution
|
|
128 |
|
|
129 |
if [ -n "$UNOFFICIAL" ]; then
|
|
130 |
{
|
|
131 |
echo
|
|
132 |
echo "IMPORTANT NOTE"
|
|
133 |
echo "=============="
|
|
134 |
echo
|
|
135 |
echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
|
|
136 |
echo
|
|
137 |
} >UNOFFICIAL
|
|
138 |
fi
|
|
139 |
|
|
140 |
|
|
141 |
# create archive
|
|
142 |
|
|
143 |
cd $DISTBASE
|
|
144 |
|
2776
|
145 |
#FIXME doesn't work!?
|
|
146 |
#chown -R $LOGNAME:isabelle $DISTNAME
|
|
147 |
#chmod -R u+w $DISTNAME
|
|
148 |
#chmod -R g-w $DISTNAME
|
2667
|
149 |
|
|
150 |
tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz
|
|
151 |
|
|
152 |
|
|
153 |
# final note
|
|
154 |
|
|
155 |
echo
|
|
156 |
echo "That's it. You'll find the distribution in $DISTBASE."
|
|
157 |
echo
|