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