49 } |
43 } |
50 |
44 |
51 |
45 |
52 ## process command line |
46 ## process command line |
53 |
47 |
54 [ "$#" -ne 1 -a "$#" -ne 2 ] && usage |
48 # options |
55 |
49 |
56 VERSION="$1"; shift |
50 RELEASE="" |
57 |
51 |
58 if [ "$#" -eq 0 ]; then |
52 while getopts "r:" OPT |
59 DISTNAME="" |
53 do |
60 else |
54 case "$OPT" in |
61 DISTNAME="$1"; shift |
55 r) |
62 fi |
56 RELEASE="$OPTARG" |
|
57 ;; |
|
58 \?) |
|
59 usage |
|
60 ;; |
|
61 esac |
|
62 done |
|
63 |
|
64 shift $(($OPTIND - 1)) |
|
65 |
|
66 |
|
67 # args |
|
68 |
|
69 VERSION="" |
|
70 [ "$#" -gt 0 ] && { VERSION="$1"; shift; } |
|
71 [ -z "$VERSION" ] && VERSION="$RELEASE" |
|
72 [ -z "$VERSION" ] && VERSION="tip" |
|
73 |
|
74 [ "$#" -gt 0 ] && usage |
63 |
75 |
64 |
76 |
65 ## main |
77 ## main |
66 |
78 |
67 # dist version |
79 # tmp |
|
80 |
|
81 TMP="tmp-$USER$$" |
|
82 function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; } |
|
83 |
|
84 |
|
85 # retrieve archive and resolve version identifier |
|
86 |
|
87 mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory" |
|
88 cd "$DISTPREFIX/$TMP" |
|
89 |
|
90 echo "###" |
|
91 echo "### Retrieving Mercurial repository $VERSION" |
|
92 echo "###" |
|
93 |
|
94 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \ |
|
95 fail "Failed to retrieve $VERSION" |
|
96 |
|
97 IDENT=$(echo * | sed 's/isabelle-//') |
|
98 |
|
99 rm -f "isabelle-$IDENT/.hg_archival.txt" |
|
100 rm -f "isabelle-$IDENT/.hgtags" |
|
101 rm -f "isabelle-$IDENT/.hgignore" |
|
102 rm -f "isabelle-$IDENT/README_REPOSITORY" |
|
103 |
|
104 |
|
105 # dist name |
68 |
106 |
69 DATE=$(env LC_ALL=C date "+%d-%b-%Y") |
107 DATE=$(env LC_ALL=C date "+%d-%b-%Y") |
70 DISTDATE=$(env LC_ALL=C date "+%B %Y") |
108 DISTDATE=$(env LC_ALL=C date "+%B %Y") |
71 |
109 |
72 if [ "$VERSION" = "-" ]; then |
110 if [ -z "$RELEASE" ]; then |
73 DISTIDENT="Isabelle_$DATE" |
111 DISTNAME="Isabelle_$DATE" |
74 [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" |
112 DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)" |
75 DISTVERSION="$DISTNAME" |
|
76 EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" |
|
77 UNOFFICIAL=true |
|
78 else |
113 else |
79 DISTIDENT="$VERSION" |
114 DISTNAME="$RELEASE" |
80 [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" |
|
81 DISTVERSION="$DISTNAME: $DISTDATE" |
115 DISTVERSION="$DISTNAME: $DISTDATE" |
82 EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle" |
|
83 UNOFFICIAL="" |
|
84 fi |
116 fi |
85 |
117 |
86 DISTBASE="$DISTPREFIX/dist-$DISTNAME" |
118 DISTBASE="$DISTPREFIX/dist-$DISTNAME" |
87 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!" |
119 mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; } |
88 [ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!" |
120 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; } |
89 [ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!" |
121 [ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; } |
90 |
|
91 |
|
92 # export repository |
|
93 |
|
94 echo "###" |
|
95 echo "### Exporting $DISTIDENT ..." |
|
96 echo "###" |
|
97 |
122 |
98 cd "$DISTBASE" |
123 cd "$DISTBASE" |
99 |
124 mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME" |
100 $EXPORT || fail "Export failed!" |
125 purge_tmp |
101 |
126 |
102 if [ -n "$CVS2CL" -a -n "$UNOFFICIAL" ]; then |
127 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME" |
103 cd $DISTNAME |
128 |
104 $CVS2CL |
129 |
105 gzip ChangeLog |
130 # website |
106 cp ChangeLog.gz .. |
131 |
107 cd .. |
132 mkdir -p ../website |
108 fi |
133 cat > ../website/distinfo.mak <<EOF |
109 |
134 # this is a generated file - do not edit unless you know what you are doing! |
110 find . -name CVS -print | xargs rm -rf |
135 DISTNAME=$DISTNAME |
|
136 DISTBASE=$DISTBASE |
|
137 EOF |
|
138 |
|
139 cp lib/html/library_index_content.template ../website/ |
|
140 |
|
141 |
|
142 # prepare dist for release |
|
143 |
|
144 echo "###" |
|
145 echo "### Preparing distribution $DISTNAME" |
|
146 echo "###" |
|
147 |
111 find . -name .cvsignore -print | xargs rm -rf |
148 find . -name .cvsignore -print | xargs rm -rf |
112 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x |
149 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x |
113 find . -print | xargs chmod u+rw |
150 find . -print | xargs chmod u+rw |
114 |
151 |
115 |
152 ./Admin/build all || fail "Failed to build distribution" |
116 # build components |
153 rm -rf Admin |
117 |
154 |
118 "$DISTBASE/$DISTNAME/Admin/build" all || fail "Failed to build distribution" |
155 MOVE=$(find doc-src \( -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') |
119 |
156 mv -f $MOVE doc |
120 |
157 rm doc/Isa-logics.eps |
121 # prepare dist dir for release |
158 rm doc/codegen_process.pdf |
122 |
159 rm -rf doc-src |
123 echo "###" |
160 |
124 echo "### Preparing distribution ..." |
161 mkdir contrib |
125 echo "###" |
|
126 |
|
127 cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME" |
|
128 |
|
129 mkdir -p ../website |
|
130 cat > ../website/distinfo.mak <<EOF |
|
131 # this is a generated file - do not edit unless you know what you are doing! |
|
132 |
|
133 DISTNAME=$DISTNAME |
|
134 DISTIDENT=$DISTIDENT |
|
135 DISTBASE=$DISTBASE |
|
136 EOF |
|
137 |
|
138 cp Distribution/lib/html/library_index_content.template ../website/ |
|
139 |
|
140 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') |
|
141 mv -f $MOVE Distribution/doc |
|
142 rm Distribution/doc/Isa-logics.eps |
|
143 rm Distribution/doc/codegen_process.pdf |
|
144 rm -rf Doc |
|
145 |
|
146 mkdir src contrib |
|
147 mv $SRCS src |
|
148 |
|
149 mv Distribution/* . |
|
150 rmdir Distribution |
|
151 |
|
152 |
162 |
153 cp doc/isabelle*.eps lib/logo |
163 cp doc/isabelle*.eps lib/logo |
154 |
164 |
155 |
165 |
156 if [ -n "$UNOFFICIAL" ]; then |
166 if [ -z "$RELEASE" ]; then |
157 { |
167 { |
158 echo |
168 echo |
159 echo "IMPORTANT NOTE" |
169 echo "IMPORTANT NOTE" |
160 echo "==============" |
170 echo "==============" |
161 echo |
171 echo |
162 echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE." |
172 echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE." |
|
173 echo "See $REPOS/log/$IDENT for details." |
163 echo |
174 echo |
164 } >ANNOUNCE |
175 } >ANNOUNCE |
165 else |
176 else |
166 perl -pi -e "s/val is_official = false/val is_official = true/" src/Pure/ROOT.ML |
177 perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML |
167 fi |
178 fi |
168 |
179 |
169 perl -pi -e "s/ISABELLE_IDENTIFIER=\"\"/ISABELLE_IDENTIFIER=\"$DISTNAME\"/g;" lib/scripts/getsettings |
180 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML |
170 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/library_index_header.template |
181 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings |
171 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version |
182 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template |
172 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README |
183 perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version |
173 |
184 perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README |
174 |
185 |
175 rm -rf Admin |
186 |
176 |
187 # create archives |
177 |
|
178 # create archive |
|
179 |
188 |
180 echo "###" |
189 echo "###" |
181 echo "### Creating archives ..." |
190 echo "### Creating archives ..." |
182 echo "###" |
191 echo "###" |
183 |
192 |
184 cd "$DISTBASE" |
193 cd "$DISTBASE" |
185 |
194 |
186 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST |
195 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST |
|
196 echo "$IDENT" >../ISABELLE_IDENT |
187 |
197 |
188 rm -f Isabelle |
198 rm -f Isabelle |
189 ln -s "$DISTNAME" Isabelle |
199 ln -s "$DISTNAME" Isabelle |
190 |
200 |
191 chown -R "$LOGNAME" "$DISTNAME" |
201 chown -R "$LOGNAME" "$DISTNAME" |