1#!/usr/bin/env bash
2#
3# Author: Makarius
4#
5# DESCRIPTION: make Isabelle distribution from repository
6
7## global parameters
8
9umask 022
10
11HG="${HG:-hg}"
12
13DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
14
15
16## diagnostics
17
18PRG="$(basename "$0")"
19
20function usage()
21{
22  echo
23  echo "Usage: isabelle $PRG [OPTIONS] [VERSION]"
24  echo
25  echo "  Options are:"
26  echo "    -O           official release (not release-candidate)"
27  echo "    -d DIR       global directory prefix (default: \"$DISTPREFIX\")"
28  echo "    -j INT       maximum number of parallel jobs (default 1)"
29  echo "    -r RELEASE   proper release with name"
30  echo
31  echo "  Make Isabelle distribution from the local repository clone."
32  echo
33  echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
34  echo "  the default is RELEASE if given, otherwise \"tip\"."
35  echo
36  echo "  Add-on components are that of the running Isabelle version!"
37  echo
38  exit 1
39}
40
41function fail()
42{
43  echo "$1" >&2
44  exit 2
45}
46
47function check_number()
48{
49  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
50}
51
52
53## process command line
54
55# options
56
57OFFICIAL_RELEASE="false"
58JOBS=""
59RELEASE=""
60
61while getopts "Od:j:r:" OPT
62do
63  case "$OPT" in
64    O)
65      OFFICIAL_RELEASE="true"
66      ;;
67    d)
68      DISTPREFIX="$OPTARG"
69      ;;
70    j)
71      check_number "$OPTARG"
72      JOBS="-j $OPTARG"
73      ;;
74    r)
75      RELEASE="$OPTARG"
76      ;;
77    \?)
78      usage
79      ;;
80  esac
81done
82
83shift $(($OPTIND - 1))
84
85
86# args
87
88VERSION=""
89[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
90[ -z "$VERSION" ] && VERSION="$RELEASE"
91[ -z "$VERSION" ] && VERSION="tip"
92
93[ "$#" -gt 0 ] && usage
94
95IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i)
96[ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\""
97
98
99## main
100
101# dist name
102
103DATE=$(env LC_ALL=C date "+%d-%b-%Y")
104DISTDATE=$(env LC_ALL=C date "+%B %Y")
105
106if [ -z "$RELEASE" ]; then
107  DISTNAME="Isabelle_$DATE"
108  DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
109else
110  DISTNAME="$RELEASE"
111  DISTVERSION="$DISTNAME: $DISTDATE"
112fi
113
114DISTPREFIX="$(cd "$DISTPREFIX"; pwd)"
115DISTBASE="$DISTPREFIX/dist-$DISTNAME"
116mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\""
117
118DIR="$DISTBASE/$DISTNAME"
119[ -e "$DIR" ] && fail "Directory \"$DIR\" already exists"
120
121rm -f "$DISTPREFIX/ISABELLE_DIST" "$DISTPREFIX/ISABELLE_IDENT"
122
123
124# retrieve repository archive
125
126echo "### Retrieving Mercurial repository version $VERSION"
127
128"$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \
129  fail "Failed to retrieve $VERSION"
130
131rm -f "$DIR/.hg_archival.txt"
132rm -f "$DIR/.hgtags"
133rm -f "$DIR/.hgignore"
134rm -f "$DIR/README_REPOSITORY"
135
136
137# partial context switch to new version
138
139cd "$DIR"
140
141unset ISABELLE_SETTINGS_PRESENT
142unset ISABELLE_SITE_SETTINGS_PRESENT
143
144if [ -z "$RELEASE" ]; then
145  {
146    echo
147    echo "IMPORTANT NOTE"
148    echo "=============="
149    echo
150    echo "This is a snapshot of Isabelle/${IDENT} from the repository."
151    echo
152  } >ANNOUNCE
153fi
154
155if [ -n "$RELEASE" -a "$OFFICIAL_RELEASE" = true ]; then
156  IS_OFFICIAL="true"
157else
158  IS_OFFICIAL="false"
159fi
160
161perl -pi \
162  -e "s,val is_identified = false,val is_identified = true,g;" \
163  -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g;" \
164  src/Pure/System/distribution.ML src/Pure/System/distribution.scala
165
166perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
167perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
168perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
169perl -pi -e "s,repository version,$DISTVERSION,g" \
170  src/Pure/System/distribution.ML src/Pure/System/distribution.scala lib/Tools/version
171perl -pi -e "s,some repository version of Isabelle,$DISTVERSION,g" README
172
173mkdir -p contrib
174cat >contrib/README <<EOF
175This directory contains add-on components that contribute to the main
176Isabelle distribution.  Separate licensing conditions apply, see each
177directory individually.
178EOF
179
180
181# prepare dist for release
182
183echo "### Preparing distribution $DISTNAME"
184
185find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -print | xargs chmod -f -x
186find . -print | xargs chmod -f u+rw
187
188export CLASSPATH="$ISABELLE_CLASSPATH"
189
190./Admin/build all || fail "Failed to build distribution"
191
192./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
193
194cp -a src src.orig
195env ISABELLE_IDENTIFIER="${DISTNAME}-build" \
196  ./bin/isabelle build_doc $JOBS -s -a || fail "Failed to build documentation"
197rm -rf src
198mv src.orig src
199
200./bin/isabelle news
201
202rm -rf Admin browser_info heaps
203
204rmdir "$USER_HOME/.isabelle/${DISTNAME}-build"
205rmdir "$USER_HOME/.isabelle/${DISTNAME}"
206
207
208# create archive
209
210#GNU tar (notably on Mac OS X)
211type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
212
213echo "### Creating archive"
214
215cd "$DISTBASE"
216
217echo "$DISTBASE/$DISTNAME.tar.gz" > "$DISTPREFIX/ISABELLE_DIST"
218echo "$IDENT" > "$DISTPREFIX/ISABELLE_IDENT"
219
220chown -R "$LOGNAME" "$DISTNAME"
221chmod -R g=o "$DISTNAME"
222chmod -R u+w "$DISTNAME"
223find "$DISTNAME" -type f "(" -name '*.scala' -o -name '*.ML' -o -name '*.thy' ")" -print | xargs chmod -f u-w
224
225echo "$DISTBASE/$DISTNAME.tar.gz"
226tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
227[ "$?" = 0 ] || exit "$?"
228
229
230# cleanup dist
231
232mv "$DISTNAME" "${DISTNAME}-old"
233mkdir "$DISTNAME"
234
235mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
236  "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
237mkdir "$DISTNAME/doc"
238mv "${DISTNAME}-old/doc/"*.pdf \
239  "${DISTNAME}-old/doc/"*.html \
240  "${DISTNAME}-old/doc/"*.css \
241  "${DISTNAME}-old/doc/fonts" \
242  "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
243
244rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
245
246rm -rf "${DISTNAME}-old"
247